case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹
by_cases ha : a = 0
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
by_cases hx : x = 0
no goals
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
simp only [ha, zero_left]
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a y x' y' : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
subst x
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a y x' y' : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a y x' y' : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹
simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
no goals
case pos
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a y x' y' : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹
simp [h.resolve_right ha]
case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
have := mul_ne_zero ha hx
case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
rw [h.eq, mul_ne_zero_iff] at this
no goals
case neg
α : Type ?u.1223
M₀ : Type ?u.1226
G₀ : Type u_1
M₀' : Type ?u.1232
G₀' : Type ?u.1235
F : Type ?u.1238
F' : Type ?u.1241
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h