harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma RightHomologyData.exact_iff_mono_g' [S.HasHomology] (h : RightHomologyData S) :
    S.Exact ↔ Mono h.g'

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
a✝ : Mono h.g'
⊢ S.Exact

Tactic:
simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_mono h.ι, ← cancel_mono h.g',
  id_comp, h.ι_g', zero_comp]

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact → Mono h.g'

Tactic:
intro hS

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
hS : S.Exact
⊢ Mono h.g'

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ Mono h.g' → S.Exact

Tactic:
intro

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
a✝ : Mono h.g'
⊢ S.Exact

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
hS : S.Exact
⊢ Mono h.g'

Tactic:
exact hS.mono_g' h

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact ↔ Mono h.g'

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact → Mono h.g'

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ Mono h.g' → S.Exact
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem minpoly_add_algebraMap_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (x + algebraMap K L r)).Splits (algebraMap K L)

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) (minpoly K (x + (algebraMap K L) r))

Tactic:
simpa [minpoly.add_algebraMap] using g.comp_X_sub_C r

Result:
no goals
-- Mathlib/RingTheory/Ideal/Defs.lean
lemma mem_of_dvd (hab : a ∣ b) (ha : a ∈ I) : b ∈ I

Proof state:
α : Type u
a b : α
inst✝ : CommSemiring α
I : Ideal α
hab : a ∣ b
ha : a ∈ I
⊢ b ∈ I

Tactic:
obtain ⟨c, rfl⟩ := hab

Result:
case intro
α : Type u
a : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I

Proof state:
case intro
α : Type u
a : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I

Tactic:
exact I.mul_mem_right _ ha

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_support_card_lt (h : f ≠ 0) : #(eraseLead f).support < #f.support

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support < #f.support

Tactic:
rw [eraseLead_support]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support

Tactic:
exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.Inv_constToCNF (heq : aig.decls[upper] = .const b) :
    State.Inv (aig := aig) (Decl.constToCNF (.inr ⟨upper, h⟩) b)

Proof state:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig assign1) (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b)

Tactic:
simp [CNF.sat_def, denote_idx_const heq]

Result:
no goals

Proof state:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
⊢ Inv (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b)

Tactic:
intro assign1

Result:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig assign1) (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b)
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ioc_pred_pred_eq_Ico_of_not_isMin (ha : ¬ IsMin a) (b : α) :
    Ioc (pred a) (pred b) = Ico a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) (pred b) = Ico a b

Tactic:
rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem card_rootSet_eq_natDegree_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0)
    (h : f.Splits (algebraMap F K)) : Fintype.card (f.rootSet K) = f.natDegree ↔ f.Separable

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (algebraMap F K) f
⊢ Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable

Tactic:
classical
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, natDegree_eq_card_roots h,
  Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]

Result:
no goals

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (algebraMap F K) f
⊢ Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable

Tactic:
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, natDegree_eq_card_roots h,
  Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem prod_roots_eq_coeff_zero_of_monic_of_splits {P : K[X]} (hmo : P.Monic)
    (hP : P.Splits (RingHom.id K)) : coeff P 0 = (-1) ^ P.natDegree * P.roots.prod

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (eval 0 ∘ fun a => X - C a) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod

Tactic:
simp_rw [Function.comp_apply, eval_sub, eval_X, zero_sub, eval_C]

Result:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun x => -x) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun x => -x) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod

Tactic:
conv_lhs =>
  congr
  congr
  ext
  rw [neg_eq_neg_one_mul]

Result:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (HMul.hMul (-1)) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

Tactic:
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]

Result:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun a => X - C a) P.roots).prod.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (HMul.hMul (-1)) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod

Tactic:
simp only [splits_iff_card_roots.1 hP, neg_mul, one_mul, Multiset.prod_map_neg]

Result:
no goals

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun a => X - C a) P.roots).prod.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

Tactic:
rw [coeff_zero_eq_eval_zero, eval_multiset_prod, Multiset.map_map]

Result:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (eval 0 ∘ fun a => X - C a) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_pow {a : ℝ≥0∞} : expGrowthInf (fun n ↦ a ^ n) = log a

Proof state:
a : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
⊢ (a ^ n).log / ↑n = a.log

Tactic:
rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
  (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ liminf (fun n => (a ^ n).log / ↑n) atTop = liminf (fun x => a.log) atTop

Tactic:
refine liminf_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)

Result:
a : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
⊢ (a ^ n).log / ↑n = a.log

Proof state:
a : ℝ≥0∞
⊢ (expGrowthInf fun n => a ^ n) = a.log

Tactic:
rw [expGrowthInf, ← liminf_const (f := atTop (α := ℕ)) (log a)]

Result:
a : ℝ≥0∞
⊢ liminf (fun n => (a ^ n).log / ↑n) atTop = liminf (fun x => a.log) atTop
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_apply_le_of_tendsto {C : ℝ} {F : ι → lp E ∞} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C)
    {f : ∀ a, E a} (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (a : α) : ‖f a‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)
⊢ ∀ (x : ι), ‖F x‖ ≤ C → ‖↑(F x) a‖ ≤ C

Tactic:
intro k hCFk

Result:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)
k : ι
hCFk : ‖F k‖ ≤ C
⊢ ‖↑(F k) a‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
⊢ ‖f a‖ ≤ C

Tactic:
have : Tendsto (fun k => ‖F k a‖) l (𝓝 ‖f a‖) :=
  (Tendsto.comp (continuous_apply a).continuousAt hf).norm

Result:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)
⊢ ‖f a‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)
k : ι
hCFk : ‖F k‖ ≤ C
⊢ ‖↑(F k) a‖ ≤ C

Tactic:
exact (norm_apply_le_norm ENNReal.top_ne_zero (F k) a).trans hCFk

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)
⊢ ‖f a‖ ≤ C

Tactic:
refine le_of_tendsto this (hCF.mono ?_)

Result:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
a : α
this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)
⊢ ∀ (x : ι), ‖F x‖ ≤ C → ‖↑(F x) a‖ ≤ C
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_succ_le_succ_sqrt (n : ℕ) : sqrt n.succ ≤ n.sqrt.succ :=
  le_of_lt_succ <| sqrt_lt.2 <| lt_succ_of_le <|
  succ_le_succ <| le_trans (sqrt_le_add n) <| Nat.add_le_add_right
    (by refine add_le_add (Nat.mul_le_mul_right _ ?_) ?_ <;> exact Nat.le_add_right _ 2) _

Proof state:
n : ℕ
⊢ n.sqrt * n.sqrt + n.sqrt ≤ n.sqrt.succ.succ.mul (n.sqrt + 1)

Tactic:
refine add_le_add (Nat.mul_le_mul_right _ ?_) ?_ <;> exact Nat.le_add_right _ 2

Result:
no goals
-- Mathlib/RingTheory/Filtration.lean
theorem submodule_fg_iff_stable (hF' : ∀ i, (F.N i).FG) : F.submodule.FG ↔ F.Stable

Proof state:
case mp.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ iSup
      ⇑{ toFun := fun n₀ => Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)),
          monotone' := ⋯ } =
    F.submodule

Tactic:
dsimp

Result:
case mp.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ ⨆ n₀, Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) = F.submodule

Proof state:
case mp.refine_2.e_s.h.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ (∃ i, ∃ x ∈ F.N i, (single R i) x = x✝) → ∃ i, ∃ i_1 ≤ i, ∃ x ∈ F.N i_1, (single R i_1) x = x✝

Tactic:
rintro ⟨i, e⟩

Result:
case mp.refine_2.e_s.h.mpr.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
i : ℕ
e : ∃ x ∈ F.N i, (single R i) x = x✝
⊢ ∃ i, ∃ i_1 ≤ i, ∃ x ∈ F.N i_1, (single R i_1) x = x✝

Proof state:
case mp.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m

Tactic:
exact hi.trans e

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem eqToIso_refl {n : ℕ} (h : n = n) : X.eqToIso h = Iso.refl _

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ (X.eqToIso h).hom = (Iso.refl (X _⦋n⦌)).hom

Tactic:
simp [eqToIso]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ X.eqToIso h = Iso.refl (X _⦋n⦌)

Tactic:
ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ (X.eqToIso h).hom = (Iso.refl (X _⦋n⦌)).hom
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Pi.map_comp_map' {f g : α → C} {h : β → C} [HasProduct f] [HasProduct g] [HasProduct h]
    (p : β → α) (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (b : β), g (p b) ⟶ h b) :
    Pi.map q ≫ Pi.map' p q' = Pi.map' p (fun b => q (p b) ≫ q' b)

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
⊢ map q ≫ map' p q' = map' p fun b => q (p b) ≫ q' b

Tactic:
ext

Result:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
b✝ : β
⊢ (map q ≫ map' p q') ≫ π h b✝ = (map' p fun b => q (p b) ≫ q' b) ≫ π h b✝

Proof state:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
b✝ : β
⊢ (map q ≫ map' p q') ≫ π h b✝ = (map' p fun b => q (p b) ≫ q' b) ≫ π h b✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
theorem isLocalMin_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
    (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
    (h₀ : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁ : ∀ᶠ x in 𝓝[>] b, 0 ≤ deriv f x) :
    IsLocalMin f b :=
  isLocalMin_of_deriv' h (nhdsLT_le_nhdsNE _ (by tauto)) (nhdsGT_le_nhdsNE _ (by tauto)) h₀ h₁

Proof state:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd : ∀ᶠ (x : ℝ) in 𝓝[≠] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, 0 ≤ deriv f x
⊢ {x | (fun x => DifferentiableAt ℝ f x) x} ∈ 𝓝[≠] b

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
lemma iSup_induction {ι} (N : ι → LieSubmodule R L M) {C : M → Prop} {x : M}
    (hx : x ∈ ⨆ i, N i) (hN : ∀ i, ∀ y ∈ N i, C y) (h0 : C 0)
    (hadd : ∀ y z, C y → C z → C (y + z)) : C x

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : M → Prop
x : M
hx : x ∈ ⨆ i, ↑(N i)
hN : ∀ (i : ι), ∀ y ∈ N i, C y
h0 : C 0
hadd : ∀ (y z : M), C y → C z → C (y + z)
⊢ C x

Tactic:
exact Submodule.iSup_induction (C := C) (fun i ↦ (N i : Submodule R M)) hx hN h0 hadd

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : M → Prop
x : M
hx : x ∈ ⨆ i, N i
hN : ∀ (i : ι), ∀ y ∈ N i, C y
h0 : C 0
hadd : ∀ (y z : M), C y → C z → C (y + z)
⊢ C x

Tactic:
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
C : M → Prop
x : M
hx : x ∈ ⨆ i, ↑(N i)
hN : ∀ (i : ι), ∀ y ∈ N i, C y
h0 : C 0
hadd : ∀ (y z : M), C y → C z → C (y + z)
⊢ C x
-- Mathlib/Data/Fin/Tuple/Reflection.lean
theorem sum_eq [AddCommMonoid α] : ∀ {m} (a : Fin m → α), sum a = ∑ i, a i
  | 0, _ => rfl
  | 1, a => (Fintype.sum_unique a).symm
  | n + 2, a => by rw [Fin.sum_univ_castSucc, sum, sum_eq]

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ sum a = ∑ i : Fin (n + 2), a i

Tactic:
rw [Fin.sum_univ_castSucc, sum, sum_eq]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma leRec_succ' {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) :
    (leRec (motive := motive) refl le_succ_of_le (le_succ _)) = le_succ_of_le _ refl

Proof state:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl

Tactic:
rw [leRec_succ, leRec_self]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem add (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
    FinMeasAdditive μ (T + T')

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t

Tactic:
simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
⊢ T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
⊢ FinMeasAdditive μ (T + T')

Tactic:
intro s t hs ht hμs hμt hst

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
⊢ T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)

Tactic:
abel

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Coskeletal.lean
theorem isCoskeletal_iff_isIso : X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X)

Tactic:
rw [isCoskeletal_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔ IsIso ((coskAdj n).unit.app X)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔ IsIso ((coskAdj n).unit.app X)

Tactic:
exact isRightKanExtension_iff_isIso ((coskAdj n).unit.app X)
  ((coskAdj n).counit.app _) (𝟙 _) ((coskAdj n).left_triangle_components X)

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Module.lean
theorem lTensor_injective_of_exact_of_exact_of_rTensor_injective
    {M₁ M₂ M₃ N₁ N₂ N₃}
    [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃]
    [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] [AddCommGroup N₃] [Module R N₃]
    {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {g₁ : N₁ →ₗ[R] N₂} {g₂ : N₂ →ₗ[R] N₃}
    (hfexact : Exact f₁ f₂) (hfsurj : Surjective f₂)
    (hgexact : Exact g₁ g₂) (hgsurj : Surjective g₂)
    (hfinj : Injective (f₁.rTensor N₃)) (hginj : Injective (g₁.lTensor M₂)) :
    Injective (g₁.lTensor M₃)

Proof state:
case intro
R : Type u_7
inst✝¹² : CommRing R
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_4
N₂ : Type u_5
N₃ : Type u_6
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
⊢ (LinearMap.rTensor N₁ f₂) x = 0

Tactic:
have : f₂.rTensor N₂ (g₁.lTensor M₂ x) = 0 := by
  rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
    LinearMap.lTensor_comp_rTensor]

Result:
case intro
R : Type u_7
inst✝¹² : CommRing R
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_4
N₂ : Type u_5
N₃ : Type u_6
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
⊢ (LinearMap.rTensor N₁ f₂) x = 0