harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
theorem N₁Γ₀_inv_app (K : ChainComplex C ℕ) :
    N₁Γ₀.inv.app K = (toKaroubi _).map (Γ₀NondegComplexIso K).inv ≫
        (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.inv.app K =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

Tactic:
change (N₁Γ₀.app K).inv = _

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

Tactic:
simp only [N₁Γ₀_app]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem counit_tensorObj :
    Coalgebra.counit (R := R) (A := (CoalgebraCat.of R M ⊗ CoalgebraCat.of R N : CoalgebraCat R))
      = Coalgebra.counit (A := M ⊗[R] N)

Proof state:
R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.counit = CoalgebraStruct.counit

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (ofList l).getKey! k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (ofList l).getKey! k' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_algebraMap (r : R) : d⌋algebraMap R (CliffordAlgebra Q) r = 0

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx

Tactic:
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r) = 0

Tactic:
refine (foldr'_algebraMap _ _ ?_ _ _).trans <| smul_zero _

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem inter_right_comm (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂ :=
  ext fun _ => by simp only [mem_inter, and_right_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ s₃ ∩ s₂

Tactic:
simp only [mem_inter, and_right_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma pOpcycles_extendOpcyclesIso_hom :
    (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom =
      (K.extendXIso e hj').hom ≫ K.pOpcycles j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom = (K.extendXIso e hj').hom ≫ K.pOpcycles j

Tactic:
simp only [← cancel_mono (K.extendOpcyclesIso e hj').inv,
  assoc, Iso.hom_inv_id, comp_id, pOpcycles_extendOpcyclesIso_inv, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sup : y \ (x ⊔ z) = y \ x ⊓ y \ z :=
  sdiff_unique
    (calc
      y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) = ⊥

Tactic:
rw [inf_inf_sdiff, bot_inf_eq, bot_sup_eq, inf_comm (y \ z),
    inf_inf_sdiff, inf_bot_eq]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)

Tactic:
rw [sup_inf_sdiff, sup_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z)

Tactic:
rw [sup_inf_left]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z)

Tactic:
rw [inf_sup_left]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)

Tactic:
rw [@inf_sup_left _ _ y]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z))

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) = (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x)

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y

Tactic:
rw [sup_inf_self, sup_inf_self, inf_idem]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) = (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z))

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)

Tactic:
rw [inf_sup_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem join_map_filter (p : α → Bool) (l : List (List α)) :
    (l.map (filter p)).flatten = (l.flatten).filter p

Proof state:
α : Type u_1
p : α → Bool
l : List (List α)
⊢ (map (filter p) l).flatten = filter p l.flatten

Tactic:
rw [filter_flatten]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_monomial (n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
H : a ≠ 0
⊢ (Finsupp.single n a).support = {n}

Tactic:
exact Finsupp.support_single_ne_zero _ H

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
H : a ≠ 0
⊢ ((monomial n) a).support = {n}

Tactic:
rw [← ofFinsupp_single, support]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
H : a ≠ 0
⊢ (Finsupp.single n a).support = {n}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {h'} :
    get (m.erase k) a h' = get m a (contains_of_contains_erase _ h h')

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
h' : (m.erase k).contains a = true
⊢ get (m.erase k) a h' = get m a ⋯

Tactic:
simp_to_model [erase] using List.getValue_eraseKey

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
@[simp] lemma zero_ssubset : 0 ⊂ s ↔ s ≠ 0

Proof state:
α : Type u_1
s : Multiset α
⊢ 0 ⊂ s ↔ s ≠ 0

Tactic:
simp [ssubset_iff_subset_not_subset]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
@[reassoc (attr := simp)]
lemma ιTotal_totalFlipIso_f_hom
    (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₂ c₁ c (i₂, i₁) = j) :
    K.flip.ιTotal c i₂ i₁ j h ≫ (K.totalFlipIso c).hom.f j =
      ComplexShape.σ c₁ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j
        (by rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, h])

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₂.π c₁ c (i₂, i₁) = j
⊢ K.flip.ιTotal c i₂ i₁ j h ≫ (K.totalFlipIso c).hom.f j = c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯

Tactic:
simp [totalFlipIso, totalFlipIsoX]

Result:
no goals

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{?u.40131, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₂.π c₁ c (i₂, i₁) = j
⊢ c₁.π c₂ c (i₁, i₂) = j

Tactic:
rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem comp_single (p : R[X]) (i : ℕ) (m : M) : comp p (single R i m) = p ^ i • single R 0 m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ p ^ i • (lsingle R 0) m = p ^ i • (single R 0) m

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ (comp p) ((single R i) m) = p ^ i • (single R 0) m

Tactic:
rw [comp_apply, map_single, eval_single]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ p ^ i • (lsingle R 0) m = p ^ i • (single R 0) m
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_X {R} [CommSemiring R] [Nontrivial R] (s : σ) :
    (X s : MvPolynomial σ R).totalDegree = 1

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ({Finsupp.single s 1}.sup fun s => s.sum fun x e => e) = 1

Tactic:
simp only [Finset.sup, Finsupp.sum_single_index, Finset.fold_singleton, sup_bot_eq]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ (X s).totalDegree = 1

Tactic:
rw [totalDegree, support_X]

Result:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ({Finsupp.single s 1}.sup fun s => s.sum fun x e => e) = 1
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightShift_add (a n' : ℤ) (hn' : n' + a = n) :
    (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn').v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn').v p q hpq + (γ₂.rightShift a n' hn').v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn').v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn').v p q hpq + (γ₂.rightShift a n' hn').v p q hpq

Tactic:
simp only [rightShift_v _ a n' hn' p q hpq _ rfl, add_v, add_comp]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
@[simp]
lemma mkOfLe_refl {n} (j : Fin (n + 1)) :
    mkOfLe j j (by omega) = ⦋1⦌.const ⦋n⦌ j := Hom.ext_one_left _ _

Proof state:
n : ℕ
j : Fin (n + 1)
⊢ j ≤ j

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem ins_toList {p : Path α} : (p.ins t).toList = p.withList t.toList

Proof state:
α : Type u_1
t : RBNode α
p : Path α
l✝ : RBNode α
v✝ : α
parent✝ : Path α
⊢ ((right black l✝ v✝ parent✝).ins t).toList = (right black l✝ v✝ parent✝).withList t.toList

Tactic:
simp [ins, ins_toList]

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
p : Path α
⊢ (p.ins t).toList = p.withList t.toList

Tactic:
match p with
| .root | .left red .. | .right red .. | .left black .. | .right black .. =>
  simp [ins, ins_toList]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem map_equiv_normalizer_eq (H : Subgroup G) (f : G ≃* N) :
    H.normalizer.map f.toMonoidHom = (H.map f.toMonoidHom).normalizer

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
⊢ map f.toMonoidHom H.normalizer = (map f.toMonoidHom H).normalizer

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ x ∈ map f.toMonoidHom H.normalizer ↔ x ∈ (map f.toMonoidHom H).normalizer

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ (a : G), (a ∈ H ↔ f.symm x * a * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a) ∈ H ↔ f.symm (x * f.toEquiv a * x⁻¹) ∈ H)

Tactic:
intro

Result:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
a✝ : G
⊢ (a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a✝) ∈ H ↔ f.symm (x * f.toEquiv a✝ * x⁻¹) ∈ H)

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ (∀ (h : G), h ∈ H ↔ f.symm x * h * (f.symm x)⁻¹ ∈ H) ↔ ∀ (h : N), f.symm h ∈ H ↔ f.symm (x * h * x⁻¹) ∈ H

Tactic:
rw [f.toEquiv.forall_congr]

Result:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ (a : G), (a ∈ H ↔ f.symm x * a * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a) ∈ H ↔ f.symm (x * f.toEquiv a * x⁻¹) ∈ H)

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
a✝ : G
⊢ (a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a✝) ∈ H ↔ f.symm (x * f.toEquiv a✝ * x⁻¹) ∈ H)

Tactic:
simp

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ x ∈ map f.toMonoidHom H.normalizer ↔ x ∈ (map f.toMonoidHom H).normalizer

Tactic:
simp only [mem_normalizer_iff, mem_map_equiv]

Result:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ (∀ (h : G), h ∈ H ↔ f.symm x * h * (f.symm x)⁻¹ ∈ H) ↔ ∀ (h : N), f.symm h ∈ H ↔ f.symm (x * h * x⁻¹) ∈ H
-- Mathlib/Data/List/Basic.lean
theorem idxOf_append_of_mem {a : α} (h : a ∈ l₁) : idxOf a (l₁ ++ l₂) = idxOf a l₁

Proof state:
case nil
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : a ∈ []
⊢ False

Tactic:
exact not_mem_nil a h

Result:
no goals

Proof state:
case neg
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
hh : ¬d₁ = a
⊢ idxOf a (d₁ :: (t₁ ++ l₂)) = idxOf a (d₁ :: t₁)

Tactic:
rw [idxOf_cons_ne _ hh, idxOf_cons_ne _ hh, ih (mem_of_ne_of_mem (Ne.symm hh) h)]

Result:
no goals

Proof state:
case cons
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
⊢ idxOf a (d₁ :: t₁ ++ l₂) = idxOf a (d₁ :: t₁)

Tactic:
rw [List.cons_append]

Result:
case cons
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
⊢ idxOf a (d₁ :: (t₁ ++ l₂)) = idxOf a (d₁ :: t₁)

Proof state:
case cons
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
⊢ idxOf a (d₁ :: (t₁ ++ l₂)) = idxOf a (d₁ :: t₁)

Tactic:
by_cases hh : d₁ = a

Result:
case pos
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
hh : d₁ = a
⊢ idxOf a (d₁ :: (t₁ ++ l₂)) = idxOf a (d₁ :: t₁)

case neg
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
hh : ¬d₁ = a
⊢ idxOf a (d₁ :: (t₁ ++ l₂)) = idxOf a (d₁ :: t₁)

Proof state:
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = idxOf a l₁

Tactic:
induction' l₁ with d₁ t₁ ih

Result:
case nil
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : a ∈ []
⊢ idxOf a ([] ++ l₂) = idxOf a []

case cons
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
⊢ idxOf a (d₁ :: t₁ ++ l₂) = idxOf a (d₁ :: t₁)

Proof state:
case nil
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : a ∈ []
⊢ idxOf a ([] ++ l₂) = idxOf a []

Tactic:
exfalso

Result:
case nil
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : a ∈ []
⊢ False

Proof state:
case pos
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
hh : d₁ = a
⊢ idxOf a (d₁ :: (t₁ ++ l₂)) = idxOf a (d₁ :: t₁)

Tactic:
iterate 2 rw [idxOf_cons_eq _ hh]

Result:
no goals

Proof state:
case pos
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : a ∈ t₁ → idxOf a (t₁ ++ l₂) = idxOf a t₁
h : a ∈ d₁ :: t₁
hh : d₁ = a
⊢ 0 = idxOf a (d₁ :: t₁)

Tactic:
rw [idxOf_cons_eq _ hh]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
lemma mem_of_mem_nsmul {a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) : a ∈ s

Proof state:
case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ n • s ∨ a ∈ s
⊢ a ∈ s

Tactic:
exact h.elim ih id

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ (n + 1) • s
⊢ a ∈ s

Tactic:
rw [succ_nsmul, mem_add] at h

Result:
case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ n • s ∨ a ∈ s
⊢ a ∈ s

Proof state:
case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0 • s
⊢ a ∈ s

Tactic:
rw [zero_nsmul] at h

Result:
case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0
⊢ a ∈ s

Proof state:
case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0
⊢ a ∈ s

Tactic:
exact absurd h (not_mem_zero _)

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
⊢ a ∈ s

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0 • s
⊢ a ∈ s

case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ (n + 1) • s
⊢ a ∈ s
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_eq_floor_add_one_iff_not_mem (a : α) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast

Proof state:
case refine_1
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
⊢ False

Tactic:
have := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm

Result:
case refine_1
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
this : ↑⌊a⌋ = ↑⌈a⌉
⊢ False

Proof state:
case refine_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : a ∉ range Int.cast
⊢ ⌊a⌋ + 1 ≤ ⌈a⌉

Tactic:
rw [Int.add_one_le_ceil_iff]

Result:
case refine_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : a ∉ range Int.cast
⊢ ↑⌊a⌋ < a

Proof state:
case refine_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : a ∉ range Int.cast
⊢ ⌈a⌉ = ⌊a⌋ + 1

Tactic:
apply le_antisymm (Int.ceil_le_floor_add_one _)

Result:
case refine_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : a ∉ range Int.cast
⊢ ⌊a⌋ + 1 ≤ ⌈a⌉

Proof state:
case refine_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : a ∉ range Int.cast
⊢ ↑⌊a⌋ < a

Tactic:
exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
this : ↑⌊a⌋ = ↑⌈a⌉
⊢ False

Tactic:
linarith [Int.cast_inj.mp this]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ range Int.cast

Tactic:
refine ⟨fun h ht => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
⊢ False

case refine_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
h : a ∉ range Int.cast
⊢ ⌈a⌉ = ⌊a⌋ + 1