harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma cotangentComplex_injective : Function.Injective P.toExtension.cotangentComplex

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
this : Function.Injective ⇑P.cotangentComplexAux
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Tactic:
simp only [PreSubmersivePresentation.cotangentComplexAux, LinearMap.coe_comp,
  LinearEquiv.coe_coe] at this

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
this :
  Function.Injective
    (⇑(Finsupp.linearEquivFunOnFinite S S P.rels) ∘
      ⇑(Finsupp.lcomapDomain P.map ⋯) ∘ ⇑P.cotangentSpaceBasis.repr ∘ ⇑P.toExtension.cotangentComplex)
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Tactic:
have := P.cotangentComplexAux_injective

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
this : Function.Injective ⇑P.cotangentComplexAux
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
this :
  Function.Injective
    (⇑(Finsupp.linearEquivFunOnFinite S S P.rels) ∘
      ⇑(Finsupp.lcomapDomain P.map ⋯) ∘ ⇑P.cotangentSpaceBasis.repr ∘ ⇑P.toExtension.cotangentComplex)
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Tactic:
exact Function.Injective.of_comp (Function.Injective.of_comp <| Function.Injective.of_comp this)

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
lemma quasiIso_ιTruncLE_iff_isSupported :
    QuasiIso (K.ιTruncLE e) ↔ K.IsSupported e

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (K.ιTruncLE e).op) ↔ K.op.IsSupported e.op

Tactic:
exact K.op.quasiIso_πTruncGE_iff_isSupported e.op

Result:
no goals

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (K.ιTruncLE e) ↔ K.IsSupported e

Tactic:
rw [← quasiIso_opFunctor_map_iff, ← isSupported_op_iff]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (K.ιTruncLE e).op) ↔ K.op.IsSupported e.op
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem Filter.Tendsto.inseparable_iff_uniformity {β} {l : Filter β} [NeBot l] {f g : β → α}
    {a b : α} (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) :
    Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)

Proof state:
α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
⊢ Inseparable a b ↔ Tendsto (fun x => (f x, g x)) l (𝓤 α)

Tactic:
refine ⟨fun h ↦ (ha.prod_mk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩

Result:
α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x => (f x, g x)) l (𝓤 α)
⊢ Inseparable a b

Proof state:
α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x => (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)

Tactic:
exact (ClusterPt.of_le_nhds (ha.prod_mk_nhds hb)).mono h

Result:
no goals

Proof state:
α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x => (f x, g x)) l (𝓤 α)
⊢ Inseparable a b

Tactic:
rw [inseparable_iff_clusterPt_uniformity]

Result:
α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun x => (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem iInf_toNonUnitalSubalgebra {ι : Sort*} (S : ι → NonUnitalStarSubalgebra R A) :
    (⨅ i, S i).toNonUnitalSubalgebra = ⨅ i, (S i).toNonUnitalSubalgebra :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
⊢ ↑(⨅ i, S i).toNonUnitalSubalgebra = ↑(⨅ i, (S i).toNonUnitalSubalgebra)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_replace [BEq α] (a : α) (b : β) (l : AssocList α β) :
    (replace a b l).toList =
    l.toList.replaceF (bif ·.1 == a then some (a, b) else none)

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
b : β
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : (replace a b tail✝).toList = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) tail✝.toList
⊢ (match key✝ == a with
      | true => cons a b tail✝
      | false => cons key✝ value✝ (replace a b tail✝)).toList =
    match bif key✝ == a then some (a, b) else none with
    | none => (key✝, value✝) :: List.replaceF (fun x => bif x.fst == a then some (a, b) else none) tail✝.toList
    | some a => a :: tail✝.toList

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
b : β
l : AssocList α β
⊢ (replace a b l).toList = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) l.toList

Tactic:
induction l <;> simp [replace]

Result:
case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
b : β
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : (replace a b tail✝).toList = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) tail✝.toList
⊢ (match key✝ == a with
      | true => cons a b tail✝
      | false => cons key✝ value✝ (replace a b tail✝)).toList =
    match bif key✝ == a then some (a, b) else none with
    | none => (key✝, value✝) :: List.replaceF (fun x => bif x.fst == a then some (a, b) else none) tail✝.toList
    | some a => a :: tail✝.toList
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
lemma natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2

Proof state:
a : ℤ
⊢ a.natAbs ≤ a.natAbs * a.natAbs

Tactic:
apply Nat.le_mul_self

Result:
no goals

Proof state:
a : ℤ
⊢ ↑a.natAbs ≤ a ^ 2

Tactic:
rw [← Int.natAbs_sq a, sq]

Result:
a : ℤ
⊢ ↑a.natAbs ≤ ↑a.natAbs * ↑a.natAbs

Proof state:
a : ℤ
⊢ ↑a.natAbs ≤ ↑a.natAbs * ↑a.natAbs

Tactic:
norm_cast

Result:
a : ℤ
⊢ a.natAbs ≤ a.natAbs * a.natAbs
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem mem_posTangentConeAt_of_frequently_mem (h : ∃ᶠ t : ℝ in 𝓝[>] 0, x + t • y ∈ s) :
    y ∈ posTangentConeAt s x

Proof state:
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
a : ℕ → ℝ
ha : Tendsto a atTop (𝓝[>] 0)
has : ∀ (n : ℕ), x + a n • y ∈ s
n : ℕ
hn : 0 < a n
⊢ y = a⁻¹ n • a n • y

Tactic:
simp [ne_of_gt hn]

Result:
no goals

Proof state:
case intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
a : ℕ → ℝ
ha : Tendsto a atTop (𝓝[>] 0)
has : ∀ (n : ℕ), x + a n • y ∈ s
⊢ Tendsto (fun n => a⁻¹ n • (fun x => a x • y) n) atTop (𝓝 y)

Tactic:
refine tendsto_const_nhds.congr' ?_

Result:
case intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
a : ℕ → ℝ
ha : Tendsto a atTop (𝓝[>] 0)
has : ∀ (n : ℕ), x + a n • y ∈ s
⊢ (fun x => y) =ᶠ[atTop] fun n => a⁻¹ n • (fun x => a x • y) n

Proof state:
case intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
a : ℕ → ℝ
ha : Tendsto a atTop (𝓝[>] 0)
has : ∀ (n : ℕ), x + a n • y ∈ s
⊢ (fun x => y) =ᶠ[atTop] fun n => a⁻¹ n • (fun x => a x • y) n

Tactic:
filter_upwards [(tendsto_nhdsWithin_iff.1 ha).2] with n (hn : 0 < a n)

Result:
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
a : ℕ → ℝ
ha : Tendsto a atTop (𝓝[>] 0)
has : ∀ (n : ℕ), x + a n • y ∈ s
n : ℕ
hn : 0 < a n
⊢ y = a⁻¹ n • a n • y

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
⊢ y ∈ posTangentConeAt s x

Tactic:
obtain ⟨a, ha, has⟩ := Filter.exists_seq_forall_of_frequently h

Result:
case intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
a : ℕ → ℝ
ha : Tendsto a atTop (𝓝[>] 0)
has : ∀ (n : ℕ), x + a n • y ∈ s
⊢ y ∈ posTangentConeAt s x
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem le_sup_iff (ha : ⊥ < a) : a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b

Proof state:
case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Tactic:
exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
apply Iff.intro

Result:
case mp
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f → ∃ b ∈ s, a ≤ f b

case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Proof state:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ (cons c t hc).sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
rw [sup_cons, le_sup_iff]

Result:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ f c ∨ a ≤ t.sup f → ∃ b ∈ cons c t hc, a ≤ f b

Proof state:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ f c ∨ a ≤ t.sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
exact fun
| Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
| Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_le_trim_iff {m₁ m₂ : OuterMeasure α} :
    m₁.trim ≤ m₂.trim ↔ ∀ s, MeasurableSet s → m₁ s ≤ m₂ s :=
  le_trim_iff.trans <| forall₂_congr fun s hs => by rw [trim_eq _ hs]

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ m₁.trim s ≤ m₂ s ↔ m₁ s ≤ m₂ s

Tactic:
rw [trim_eq _ hs]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem image_emetric_ball (h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) :
    h '' EMetric.ball x r = EMetric.ball (h x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ⇑h '' EMetric.ball x r = EMetric.ball (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_emetric_ball, symm_symm]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.congr_set (h : ContDiffWithinAt 𝕜 n f s x) {t : Set E}
    (hst : s =ᶠ[𝓝 x] t) : ContDiffWithinAt 𝕜 n f t x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : s =ᶠ[𝓝 x] t
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
apply h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_prodMap' (f : M →ₗ[R] M) (g : N →ₗ[R] N) :
    trace R (M × N) (prodMap f g) = trace R M f + trace R N g

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) (f, g) = (id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) (f, g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Tactic:
simp only [coe_comp, Function.comp_apply, prodMap_apply, coprod_apply, id_coe, id,
  prodMapLinear_apply] at h

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M × N)) (f.prodMap g) =
    { toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } ((trace R M) f) +
      { toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } ((trace R N) g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M × N)) (f.prodMap g) =
    { toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } ((trace R M) f) +
      { toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } ((trace R N) g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Tactic:
have h := LinearMap.ext_iff.1 (trace_prodMap R M N) (f, g)

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) (f, g) = (id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) (f, g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g
-- Mathlib/Data/Vector3.lean
theorem append_insert (a : α) (t : Vector3 α m) (v : Vector3 α n) (i : Fin2 (n + 1))
    (e : (n + 1) + m = (n + m) + 1) :
    insert a (t +-+ v) (Eq.recOn e (i.add m)) = Eq.recOn e (t +-+ insert a v i)

Proof state:
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
⊢ insert a (t +-+ v) (Eq.recOn e (i.add m)) = Eq.recOn e (t +-+ insert a v i)

Tactic:
refine Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e

Result:
case refine_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e✝ : n + 1 + m = n + m + 1
e : n + 1 + 0 = n + 0 + 1
⊢ insert a ([] +-+ v) (Eq.recOn e (i.add 0)) = Eq.recOn e ([] +-+ insert a v i)

case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (i.add (k + 1))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)

Proof state:
case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (i.add (k + 1))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)

Tactic:
have e' : (n + 1) + k = (n + k) + 1 := by omega

Result:
case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (i.add (k + 1))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)

Proof state:
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ n + 1 + k = n + k + 1

Tactic:
omega

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e✝ : n + 1 + m = n + m + 1
e : n + 1 + 0 = n + 0 + 1
⊢ insert a ([] +-+ v) (Eq.recOn e (i.add 0)) = Eq.recOn e ([] +-+ insert a v i)

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a (b :: t +-+ v) (Eq.recOn e' (i.add k)).fs = Eq.recOn ⋯ (b :: t +-+ insert a v i)

Tactic:
simpa [IH] using Eq.recOn e' rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_span_pair {x y z : M} :
    z ∈ span R ({x, y} : Set M) ↔ ∃ a b : R, a • x + b • y = z

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
⊢ z ∈ span R {x, y} ↔ ∃ a b, a • x + b • y = z

Tactic:
simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] ↔ False

Proof state:
n : Nat
⊢ 0 < -[n+1] ↔ False

Tactic:
simp only [Int.not_lt, iff_false]

Result:
n : Nat
⊢ -[n+1] ≤ 0

Proof state:
n : Nat
⊢ -[n+1] ≤ 0

Tactic:
constructor

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
lemma killingForm_eq :
    killingForm R I = (killingForm R L).restrict I :=
  LieSubmodule.traceForm_eq_of_le_idealizer I I <| by simp

Proof state:
R : Type u_1
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
inst✝³ : Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ I ≤ LieSubmodule.idealizer I

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem IsPrimitive.dvd_primPart_iff_dvd {p q : R[X]} (hp : p.IsPrimitive) (hq : q ≠ 0) :
    p ∣ q.primPart ↔ p ∣ q

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ p * ?m.84211 = (p * r).primPart

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ R[X]

Tactic:
rw [primPart_mul hq, hp.primPart_eq]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ p ∣ (p * r).primPart

Tactic:
apply Dvd.intro _

Result:
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ p * ?m.84211 = (p * r).primPart

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ R[X]

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q ≠ 0
⊢ p ∣ q.primPart ↔ p ∣ q

Tactic:
refine ⟨fun h => h.trans (Dvd.intro_left _ q.eq_C_content_mul_primPart.symm), fun h => ?_⟩

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q ≠ 0
h : p ∣ q
⊢ p ∣ q.primPart

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q ≠ 0
h : p ∣ q
⊢ p ∣ q.primPart

Tactic:
rcases h with ⟨r, rfl⟩

Result:
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ p ∣ (p * r).primPart
-- Mathlib/SetTheory/Game/PGame.lean
/-- `x + 0` has exactly the same moves as `x`. -/
protected lemma add_zero : ∀ (x : PGame), x + 0 ≡ x
  | mk xl xr xL xR => by
    refine Identical.of_equiv (Equiv.sumEmpty _ _) (Equiv.sumEmpty _ _) ?_ ?_ <;>
    · rintro (_ | ⟨⟨⟩⟩)
      exact PGame.add_zero _

Proof state:
case refine_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
val✝ : xr
⊢ (mk xl xr xL xR + 0).moveRight (Sum.inl val✝) ≡
    (mk xl xr xL xR).moveRight ((Equiv.sumEmpty xr PEmpty.{u_1 + 1}) (Sum.inl val✝))

Tactic:
exact PGame.add_zero _

Result:
no goals

Proof state:
case refine_2
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ ∀ (i : (mk xl xr xL xR + 0).RightMoves),
    (mk xl xr xL xR + 0).moveRight i ≡ (mk xl xr xL xR).moveRight ((Equiv.sumEmpty xr PEmpty.{u_1 + 1}) i)

Tactic:
rintro (_ | ⟨⟨⟩⟩)

Result:
case refine_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
val✝ : xr
⊢ (mk xl xr xL xR + 0).moveRight (Sum.inl val✝) ≡
    (mk xl xr xL xR).moveRight ((Equiv.sumEmpty xr PEmpty.{u_1 + 1}) (Sum.inl val✝))
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invUnitsSub_mul_X (u : Rˣ) : invUnitsSub u * X = invUnitsSub u * C R u - 1

Proof state:
case h.succ
R : Type u_1
inst✝ : Ring R
u : Rˣ
n : ℕ
⊢ (coeff R (n + 1)) (invUnitsSub u * X) = (coeff R (n + 1)) (invUnitsSub u * (C R) ↑u - 1)

Tactic:
simp [n.succ_ne_zero, pow_succ']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ invUnitsSub u * X = invUnitsSub u * (C R) ↑u - 1

Tactic:
ext (_ | n)

Result:
case h.zero
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ (coeff R 0) (invUnitsSub u * X) = (coeff R 0) (invUnitsSub u * (C R) ↑u - 1)

case h.succ
R : Type u_1
inst✝ : Ring R
u : Rˣ
n : ℕ
⊢ (coeff R (n + 1)) (invUnitsSub u * X) = (coeff R (n + 1)) (invUnitsSub u * (C R) ↑u - 1)

Proof state:
case h.zero
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ (coeff R 0) (invUnitsSub u * X) = (coeff R 0) (invUnitsSub u * (C R) ↑u - 1)

Tactic:
simp

Result:
no goals