Theorem: groupInclusionHom_injective (UnitConjecture/GroupRing.lean)

State before:
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ Function.Injective ↑(groupInclusionHom G)
Tactic:
intro _ _
State after:
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝

State before:
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
Tactic:
apply groupInclusionHom_injective'
State after:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ 1 ≠ 0

State before:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ 1 ≠ 0
Tactic:
have : (0 : F) ≠ (1 : F) := zero_ne_one
State after:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
this : 0 ≠ 1
⊢ 1 ≠ 0

State before:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
this : 0 ≠ 1
⊢ 1 ≠ 0
Tactic:
simp_all only [ne_eq, zero_ne_one, not_false_iff, one_ne_zero]
State after:
no goals