harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_update_smul_left [DecidableEq ι] [Fintype ι]
    (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
    f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Tactic:
have :
  f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
    (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x) :=
  map_piecewise_smul f _ _ _

Result:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
    (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x)
⊢ f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
    (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x)
⊢ f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Tactic:
simpa [← Function.update_smul c m] using this

Result:
no goals
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem FiniteDimensional.of_exists_primitive_element [Algebra.IsAlgebraic F E]
    (h : ∃ α : E, F⟮α⟯ = ⊤) : FiniteDimensional F E

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥F⟮α⟯
⊢ FiniteDimensional F E

Tactic:
rw [hprim] at hfin

Result:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥⊤
⊢ FiniteDimensional F E

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
⊢ FiniteDimensional F E

Tactic:
have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)

Result:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥F⟮α⟯
⊢ FiniteDimensional F E

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
⊢ FiniteDimensional F E

Tactic:
obtain ⟨α, hprim⟩ := h

Result:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
⊢ FiniteDimensional F E

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥⊤
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Filter.EventuallyEq.fderivWithin_eq_of_insert (hs : f₁ =ᶠ[𝓝[insert x s] x] f) :
    fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Tactic:
apply Filter.EventuallyEq.fderivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ f₁ x = f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ f₁ x = f x

Tactic:
exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem subset_sSup_of_within [Inhabited s] {t : Set s}
    (h' : t.Nonempty) (h'' : BddAbove t) (h : sSup ((↑) '' t : Set α) ∈ s) :
    sSup ((↑) '' t : Set α) = (@sSup s _ t : α)

Proof state:
α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddAbove t
h : sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) = ↑(sSup t)

Tactic:
simp [dif_pos, h, h', h'']

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_nat_pow_inv {p : ℕ} :
    Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) ↔ 1 < p

Proof state:
p : ℕ
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
simp only [← rpow_natCast, summable_nat_rpow_inv, Nat.one_lt_cast]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iExs [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M} :
    BoundedFormula.Realize (φ.iExs γ) v v' ↔
      ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v

Tactic:
congr

Result:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Proof state:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' ↔ ∃ i, φ.Realize (Sum.elim v i)

Tactic:
rw [← Formula.realize_iExs, iff_iff_eq]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem sum_repr' (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, ⟪b i, x⟫_𝕜 • b i = x

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, ⟪b i, x⟫_𝕜 • b i = x

Tactic:
nth_rw 2 [← (b.sum_repr x)]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, ⟪b i, x⟫_𝕜 • b i = ∑ i : ι, b.repr x i • b i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, ⟪b i, x⟫_𝕜 • b i = ∑ i : ι, b.repr x i • b i

Tactic:
simp_rw [b.repr_apply_apply x]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem nat_mod : Primrec₂ ((· % ·) : ℕ → ℕ → ℕ) :=
  (nat_sub.comp fst (nat_mul.comp snd nat_div)).to₂.of_eq fun m n => by
    apply Nat.sub_eq_of_eq_add
    simp [add_comm (m % n), Nat.div_add_mod]

Proof state:
m n : ℕ
⊢ (m, n).1 - (m, n).2 * (fun x1 x2 => x1 / x2) (m, n).1 (m, n).2 = m % n

Tactic:
apply Nat.sub_eq_of_eq_add

Result:
case h
m n : ℕ
⊢ (m, n).1 = m % n + (m, n).2 * (fun x1 x2 => x1 / x2) (m, n).1 (m, n).2

Proof state:
case h
m n : ℕ
⊢ (m, n).1 = m % n + (m, n).2 * (fun x1 x2 => x1 / x2) (m, n).1 (m, n).2

Tactic:
simp [add_comm (m % n), Nat.div_add_mod]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem Int.emultiplicity_natAbs (a : ℕ) (b : ℤ) :
    emultiplicity a b.natAbs = emultiplicity (a : ℤ) b

Proof state:
case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs

Tactic:
rw [Int.natCast_emultiplicity]

Result:
no goals

Proof state:
case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)

Tactic:
rw [emultiplicity_neg, Int.natCast_emultiplicity]

Result:
no goals

Proof state:
a : ℕ
b : ℤ
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
rcases Int.natAbs_eq b with h | h <;> conv_rhs => rw [h]

Result:
case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs

case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem sum_add (xs ys : IntList) : (xs + ys).sum = xs.sum + ys.sum

Proof state:
case cons.nil
x : Int
xs : List Int
ih : ∀ (ys : IntList), (xs + ys).sum = sum xs + ys.sum
⊢ (x :: xs + []).sum = sum (x :: xs) + sum []

Tactic:
simp

Result:
no goals

Proof state:
xs ys : IntList
⊢ (xs + ys).sum = xs.sum + ys.sum

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys => simp_all [Int.add_assoc, Int.add_left_comm]

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), (xs + ys).sum = sum xs + ys.sum
ys : IntList
⊢ (x :: xs + ys).sum = sum (x :: xs) + ys.sum

Tactic:
cases ys with
| nil => simp
| cons y ys => simp_all [Int.add_assoc, Int.add_left_comm]

Result:
no goals

Proof state:
case nil
ys : IntList
⊢ ([] + ys).sum = sum [] + ys.sum

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), (xs + ys).sum = sum xs + ys.sum
y : Int
ys : List Int
⊢ (x :: xs + y :: ys).sum = sum (x :: xs) + sum (y :: ys)

Tactic:
simp_all [Int.add_assoc, Int.add_left_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem map_singletonSubgraph (f : G →g G') {v : V} :
    Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)

Proof state:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
⊢ Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)

Tactic:
ext <;> simp only [Relation.Map, Subgraph.map_adj, singletonSubgraph_adj, Pi.bot_apply,
  exists_and_left, and_iff_left_iff_imp, IsEmpty.forall_iff, Subgraph.map_verts,
  singletonSubgraph_verts, Set.image_singleton]

Result:
case Adj.h.h.a
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ ⊥ → ∃ x, f x = x✝¹ ∧ ∃ x, f x = x✝

Proof state:
case Adj.h.h.a
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ ⊥ → ∃ x, f x = x✝¹ ∧ ∃ x, f x = x✝

Tactic:
exact False.elim

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_singleton (a : α) (i : Nat) : [a][i]? = if i = 0 then some a else none

Proof state:
α : Type u_1
a : α
i : Nat
⊢ [a][i]? = if i = 0 then some a else none

Tactic:
simp [getElem?_cons]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma lie_eq_smul_of_mem_rootSpace {α : H → K} {x : L} (hx : x ∈ rootSpace H α) (h : H) :
    ⁅h, x⁆ = α h • x

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
h : ↥H
hx : x ∈ ((ad K L) ↑h).maxGenEigenspace (α h)
⊢ ⁅h, x⁆ = α h • x

Tactic:
rw [(isSemisimple_ad_of_mem_isCartanSubalgebra
  h.property).isFinitelySemisimple.maxGenEigenspace_eq_eigenspace,
  Module.End.mem_eigenspace_iff] at hx

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
h : ↥H
hx : ((ad K L) ↑h) x = α h • x
⊢ ⁅h, x⁆ = α h • x

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
h : ↥H
hx : ((ad K L) ↑h) x = α h • x
⊢ ⁅h, x⁆ = α h • x

Tactic:
simpa using hx

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
h : ↥H
⊢ ⁅h, x⁆ = α h • x

Tactic:
replace hx : x ∈ (ad K L h).maxGenEigenspace (α h) :=
  genWeightSpace_le_genWeightSpaceOf L h α hx

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
h : ↥H
hx : x ∈ ((ad K L) ↑h).maxGenEigenspace (α h)
⊢ ⁅h, x⁆ = α h • x
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem deriv_tan_sub_id (x : ℝ) (h : cos x ≠ 0) :
    deriv (fun y : ℝ => tan y - y) x = 1 / cos x ^ 2 - 1 :=
  HasDerivAt.deriv <| by simpa using (hasDerivAt_tan h).add (hasDerivAt_id x).neg

Proof state:
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt (fun y => tan y - y) (1 / cos x ^ 2 - 1) x

Tactic:
simpa using (hasDerivAt_tan h).add (hasDerivAt_id x).neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.or_iff_not_and_not [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ a ∨ b ↔ ¬(¬a ∧ ¬b)

Tactic:
rw [← not_or, not_not]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem mk_coe (f : α →*o β) (h) : OrderMonoidHom.mk (f : α →* β) h = f

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ { toMonoidHom := ↑f, monotone' := h } a✝ = f a✝

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ { toMonoidHom := ↑f, monotone' := h } a✝ = f a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Free.lean
theorem liftAux_spec (f : X → L) (a b : lib R X) (h : FreeLieAlgebra.Rel R X a b) :
    liftAux R f a = liftAux R f b

Proof state:
case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c' : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (a✝¹ * c') = (liftAux R f) (b✝ * c')

Tactic:
simp only [liftAux_map_mul, h₂]

Result:
no goals

Proof state:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
h : Rel R X a b
⊢ (liftAux R f) a = (liftAux R f) b

Tactic:
induction h with
| lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]
| leibniz_lie a' b' c' =>
  simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
| smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
| add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
| mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
| mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]

Result:
no goals

Proof state:
case lie_self
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' : lib R X
⊢ (liftAux R f) (a' * a') = (liftAux R f) 0

Tactic:
simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]

Result:
no goals

Proof state:
case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b c' b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
h₂ : (liftAux R f) b✝ = (liftAux R f) c✝
⊢ (liftAux R f) (c' * b✝) = (liftAux R f) (c' * c✝)

Tactic:
simp only [liftAux_map_mul, h₂]

Result:
no goals

Proof state:
case leibniz_lie
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' b' c' : lib R X
⊢ (liftAux R f) (a' * (b' * c')) = (liftAux R f) (a' * b' * c' + b' * (a' * c'))

Tactic:
simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]

Result:
no goals

Proof state:
case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c' : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (a✝¹ + c') = (liftAux R f) (b✝ + c')

Tactic:
simp only [liftAux_map_add, h₂]

Result:
no goals

Proof state:
case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
b' : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (b' • a✝¹) = (liftAux R f) (b' • b✝)

Tactic:
simp only [liftAux_map_smul, h₂]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_map {k : β → α} {l : Filter β} : f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Tactic:
simp only [IsLittleO_def, isBigOWith_map]

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
/-- **Goursat's lemma** for monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃* I`. -/
@[to_additive "**Goursat's lemma** for additive monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of additive monoids. Assume that the natural maps from
`G` to both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃+ I`."]
lemma Subgroup.exists_mulEquiv_eq_graph {G : Subgroup (H × I)}
    (hG₁ : Bijective (Prod.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.snd ∘ G.subtype)) :
    ∃ e : H ≃* I, G = e.toMonoidHom.graph

Proof state:
H : Type u_2
I : Type u_3
inst✝¹ : Group H
inst✝ : Group I
G : Subgroup (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.graph

Tactic:
simpa [SetLike.ext_iff] using Submonoid.exists_mulEquiv_eq_mgraph hG₁ hG₂

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem comp_base_apply {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g).base x = g.base (f.base x)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (f ≫ g).base) x = (ConcreteCategory.hom g.base) ((ConcreteCategory.hom f.base) x)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem upperCentralSeries_mono : Monotone (upperCentralSeries G)

Proof state:
G : Type u_1
inst✝ : Group G
⊢ ∀ (n : ℕ), upperCentralSeries G n ≤ upperCentralSeries G (n + 1)

Tactic:
intro n x hx y

Result:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G n).fst

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * (y * x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G n).fst

Tactic:
exact mul_mem hx (Normal.conj_mem (upperCentralSeries_normal G n) x⁻¹ (inv_mem hx) y)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
⊢ Monotone (upperCentralSeries G)

Tactic:
refine monotone_nat_of_le_succ ?_

Result:
G : Type u_1
inst✝ : Group G
⊢ ∀ (n : ℕ), upperCentralSeries G n ≤ upperCentralSeries G (n + 1)

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G n).fst

Tactic:
rw [mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹]

Result:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * (y * x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G n).fst
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
    filterMap f l₁ ⊆ filterMap f l₂

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
x : β
⊢ (∃ a, a ∈ l₁ ∧ f a = some x) → ∃ a, a ∈ l₂ ∧ f a = some x

Tactic:
rintro ⟨a, h, w⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
x : β
a : α
h : a ∈ l₁
w : f a = some x
⊢ ∃ a, a ∈ l₂ ∧ f a = some x

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
x : β
⊢ x ∈ filterMap f l₁ → x ∈ filterMap f l₂

Tactic:
simp only [mem_filterMap]

Result:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
x : β
⊢ (∃ a, a ∈ l₁ ∧ f a = some x) → ∃ a, a ∈ l₂ ∧ f a = some x

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
x : β
a : α
h : a ∈ l₁
w : f a = some x
⊢ ∃ a, a ∈ l₂ ∧ f a = some x

Tactic:
exact ⟨a, H h, w⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
⊢ filterMap f l₁ ⊆ filterMap f l₂

Tactic:
intro x

Result:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
H : l₁ ⊆ l₂
x : β
⊢ x ∈ filterMap f l₁ → x ∈ filterMap f l₂