harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finsupp/BigOperators.lean
theorem Finset.support_sum_subset [AddCommMonoid M] (s : Finset (ι →₀ M)) :
    (s.sum id).support ⊆ Finset.sup s Finsupp.support

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (s.sum id).support ⊆ s.sup Finsupp.support

Tactic:
convert Multiset.support_sum_subset s.1

Result:
case h.e'_3.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum

Proof state:
case h.e'_3.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (s.sum id).support ⊆ s.sup Finsupp.support

Tactic:
classical convert Multiset.support_sum_subset s.1; simp

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem congr_heq {α β γ : Sort _} {f : α → γ} {g : β → γ} {x : α} {y : β}
    (h₁ : HEq f g) (h₂ : HEq x y) : f x = g y

Proof state:
case refl.refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x

Tactic:
rfl

Result:
no goals

Proof state:
case refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : HEq f g
⊢ f x = g x

Tactic:
cases h₁

Result:
case refl.refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x

Proof state:
α β : Sort u_2
γ : Sort u_3
f : α → γ
g : β → γ
x : α
y : β
h₁ : HEq f g
h₂ : HEq x y
⊢ f x = g y

Tactic:
cases h₂

Result:
case refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : HEq f g
⊢ f x = g x
-- Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
lemma tendsto_comap_im_ofComplex :
    Tendsto ofComplex (comap Complex.im atTop) atImInfty

Proof state:
⊢ Complex.im =ᶠ[comap Complex.im atTop] fun x => (↑ofComplex x).im

Tactic:
filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz

Result:
case h
z : ℂ
hz : z ∈ Complex.im ⁻¹' Set.Ioi 0
⊢ z.im = (↑ofComplex z).im

Proof state:
⊢ Tendsto (↑ofComplex) (comap Complex.im atTop) atImInfty

Tactic:
simp only [atImInfty, tendsto_comap_iff, Function.comp_def]

Result:
⊢ Tendsto (fun x => (↑ofComplex x).im) (comap Complex.im atTop) atTop

Proof state:
⊢ Tendsto (fun x => (↑ofComplex x).im) (comap Complex.im atTop) atTop

Tactic:
refine tendsto_comap.congr' ?_

Result:
⊢ Complex.im =ᶠ[comap Complex.im atTop] fun x => (↑ofComplex x).im

Proof state:
case h
z : ℂ
hz : z ∈ Complex.im ⁻¹' Set.Ioi 0
⊢ z.im = (↑ofComplex z).im

Tactic:
simp only [ofComplex_apply_of_im_pos hz, ← UpperHalfPlane.coe_im, coe_mk_subtype]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_lt_aleph0 (n : ℕ) : (n : Cardinal.{u}) < ℵ₀ :=
  succ_le_iff.1
    (by
      rw [← nat_succ, ← lift_mk_fin, aleph0, lift_mk_le.{u}]
      exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩)

Proof state:
n : ℕ
⊢ Nonempty (Fin n.succ ↪ ℕ)

Tactic:
exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩

Result:
no goals

Proof state:
n : ℕ
⊢ succ ↑n ≤ ℵ₀

Tactic:
rw [← nat_succ, ← lift_mk_fin, aleph0, lift_mk_le.{u}]

Result:
n : ℕ
⊢ Nonempty (Fin n.succ ↪ ℕ)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
    (h : m.WF) : (Const.modify m k f).getKey! k = if k ∈ m then k else default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey! k = if k ∈ m then k else default

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey! k = if m.contains k = true then k else default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey! k = if m.contains k = true then k else default

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

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_to_int [AddGroupWithOne α] : ∀ n : ZNum, ((n : ℤ) : α) = n
  | 0 => by rw [cast_zero, cast_zero, Int.cast_zero]
  | pos p => by rw [cast_pos, cast_pos, PosNum.cast_to_int]
  | neg p => by rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(neg p) = ↑(neg p)

Tactic:
rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(pos p) = ↑(pos p)

Tactic:
rw [cast_pos, cast_pos, PosNum.cast_to_int]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑↑0 = ↑0

Tactic:
rw [cast_zero, cast_zero, Int.cast_zero]

Result:
no goals
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem Prime.pow_dvd_of_dvd_mul_left [CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p)
    (n : ℕ) (h : ¬p ∣ a) (h' : p ^ n ∣ a * b) : p ^ n ∣ b

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ b

Tactic:
induction n with
| zero =>
  rw [pow_zero]
  exact one_dvd b
| succ n ih =>
  obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
  rw [pow_succ]
  apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
  rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : p ^ 0 ∣ a * b
⊢ 1 ∣ b

Tactic:
exact one_dvd b

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : p ^ 0 ∣ a * b
⊢ p ^ 0 ∣ b

Tactic:
rw [pow_zero]

Result:
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : p ^ 0 ∣ a * b
⊢ 1 ∣ b

Proof state:
case succ.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ (n + 1) ∣ p ^ n * c

Tactic:
rw [pow_succ]

Result:
case succ.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * c

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ∣ a * c

Tactic:
rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
ih : p ^ n ∣ a * b → p ^ n ∣ b
h' : p ^ (n + 1) ∣ a * b
⊢ p ^ (n + 1) ∣ b

Tactic:
obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')

Result:
case succ.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ (n + 1) ∣ p ^ n * c

Proof state:
case succ.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * c

Tactic:
apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ∣ a * c
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem toTopologicalSpace_iInf {ι : Sort*} {u : ι → UniformSpace α} :
    (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace :=
  TopologicalSpace.ext_nhds fun a ↦ by simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
    iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]

Proof state:
α : Type ua
ι : Sort u_2
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_one : adjugate (1 : Matrix n n α) = 1

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i✝ j✝ : n
⊢ adjugate 1 i✝ j✝ = 1 i✝ j✝

Tactic:
simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
⊢ adjugate 1 = 1

Tactic:
ext

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i✝ j✝ : n
⊢ adjugate 1 i✝ j✝ = 1 i✝ j✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_negY (P : Fin 3 → R) : (W'.map f).toProjective.negY (f ∘ P) = f (W'.negY P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toProjective.negY (⇑f ∘ P) = f (W'.negY P)

Tactic:
simp only [negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -(⇑f ∘ P) y - (map W' f).toProjective.a₁ * (⇑f ∘ P) x - (map W' f).toProjective.a₃ * (⇑f ∘ P) z =
    f (-P y - W'.a₁ * P x - W'.a₃ * P z)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -(⇑f ∘ P) y - (map W' f).toProjective.a₁ * (⇑f ∘ P) x - (map W' f).toProjective.a₃ * (⇑f ∘ P) z =
    f (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_univ {n : ℕ} :
    iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f

Tactic:
induction n with
| zero => ext x; simp
| succ n IH =>
  ext x m
  rw [iteratedFDeriv_succ_apply_left, iteratedFDerivWithin_succ_apply_left, IH, fderivWithin_univ]

Result:
no goals

Proof state:
case succ.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
IH : iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f
x : E
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m = (iteratedFDeriv 𝕜 (n + 1) f x) m

Tactic:
rw [iteratedFDeriv_succ_apply_left, iteratedFDerivWithin_succ_apply_left, IH, fderivWithin_univ]

Result:
no goals

Proof state:
case zero.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 f univ x) x✝ = (iteratedFDeriv 𝕜 0 f x) x✝

Tactic:
simp

Result:
no goals

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
IH : iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f
⊢ iteratedFDerivWithin 𝕜 (n + 1) f univ = iteratedFDeriv 𝕜 (n + 1) f

Tactic:
ext x m

Result:
case succ.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
IH : iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f
x : E
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m = (iteratedFDeriv 𝕜 (n + 1) f x) m

Proof state:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ iteratedFDerivWithin 𝕜 0 f univ = iteratedFDeriv 𝕜 0 f

Tactic:
ext x

Result:
case zero.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 f univ x) x✝ = (iteratedFDeriv 𝕜 0 f x) x✝
-- Mathlib/SetTheory/Cardinal/ENat.lean
lemma toENat_strictMonoOn : StrictMonoOn toENat (Iic ℵ₀)

Proof state:
⊢ ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1

Tactic:
exact fun _ _ ↦ id

Result:
no goals

Proof state:
⊢ StrictMonoOn (⇑toENat) (Iic ℵ₀)

Tactic:
simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]

Result:
⊢ ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preOmega_natCast (n : ℕ) : preOmega n = n

Proof state:
case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) = ↑(n + 1)

Tactic:
apply (le_preOmega_self _).antisymm'

Result:
case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) ≤ ↑(n + 1)

Proof state:
n : ℕ
⊢ preOmega ↑n = ↑n

Tactic:
induction n with
| zero => exact preOmega_zero
| succ n IH =>
  apply (le_preOmega_self _).antisymm'
  apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)
  rw [Nat.cast_lt]
  exact lt_succ n

Result:
no goals

Proof state:
case zero

⊢ preOmega ↑0 = ↑0

Tactic:
exact preOmega_zero

Result:
no goals

Proof state:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1

Tactic:
exact lt_succ n

Result:
no goals

Proof state:
case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) ≤ ↑(n + 1)

Tactic:
apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)

Result:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ ↑n < ↑(n + 1)

Proof state:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ ↑n < ↑(n + 1)

Tactic:
rw [Nat.cast_lt]

Result:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1
-- Mathlib/Algebra/Order/Group/Action.lean
lemma le_pow_smul {G : Type*} [Monoid G] {α : Type*} [Preorder α] {g : G} {a : α}
    [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le]
    (h : a ≤ g • a) (n : ℕ) : a ≤ g ^ n • a

Proof state:
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
⊢ a ≤ g ^ n • a

Tactic:
induction' n with n hn

Result:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ g ^ 0 • a

case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g ^ (n + 1) • a

Proof state:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g ^ (n + 1) • a

Tactic:
rw [pow_succ', mul_smul]

Result:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g • g ^ n • a

Proof state:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ g ^ 0 • a

Tactic:
rw [pow_zero, one_smul]

Result:
no goals

Proof state:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g • g ^ n • a

Tactic:
exact h.trans (smul_mono_right g hn)

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.sum (h : ∀ i ∈ s, A i =o[l] g') : (fun x => ∑ i ∈ s, A i x) =o[l] g'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ (fun x => ∑ i ∈ s, A i x) =o[l] g'

Tactic:
simp only [← Finset.sum_apply]

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ (fun x => (∑ c ∈ s, A c) x) =o[l] g'
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudoEqual_trans {P : C} : Transitive (PseudoEqual P)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
⊢ Transitive (PseudoEqual P)

Tactic:
intro f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst q p' ≫ p) ≫ f.hom = (pullback.snd q p' ≫ q') ≫ h.hom

Tactic:
rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
  Category.assoc]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h

Tactic:
refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
  epi_comp _ _, epi_comp _ _, ?_⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst q p' ≫ p) ≫ f.hom = (pullback.snd q p' ≫ q') ≫ h.hom
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_eq_one_of_le (h : B ≤ A) : relfinrank A B = 1

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : B ≤ A
⊢ A.relfinrank B = 1

Tactic:
simp [relfinrank_eq_toNat_relrank, relrank_eq_one_of_le h]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.locPathConnectedSpace [LocPathConnectedSpace H] : LocPathConnectedSpace M

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let e := chartAt H x

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → M)
    (hf : ContMDiffAt (J.prod I) I' n (Function.uncurry f) (x₀, g x₀)) (hg : ContMDiffAt J I m g x₀)
    (hmn : m + 1 ≤ n) :
    haveI : IsManifold I 1 M := .of_le (le_trans le_add_self hmn)
    haveI : IsManifold I' 1 M' := .of_le (le_trans le_add_self hmn)
    ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m
      (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv I I' (f x) (g x)) x₀)
      x₀

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J n N
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)
hg : ContMDiffAt J I m g x₀
hmn : m + 1 ≤ n
⊢ ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hf hg ⊢

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J n N
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) univ x₀
-- Mathlib/Data/Multiset/Fintype.lean
lemma coe_consEquiv_of_eq_of_lt {v : α} (x : v ::ₘ m) (hx : ↑x = v) (hx2 : x.2 < m.count v) :
    consEquiv x = some ⟨x.1, ⟨x.2, by simpa [hx]⟩⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst = v
hx2 : ↑x.snd < count v m
⊢ consEquiv x = some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩

Tactic:
simp [consEquiv, hx, hx2.ne]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst = v
hx2 : ↑x.snd < count v m
⊢ ↑x.snd < count x.fst m

Tactic:
simpa [hx]

Result:
no goals
-- Mathlib/Algebra/Homology/Additive.lean
theorem singleMapHomologicalComplex_hom_app_self (j : ι) (X : W₁) :
    ((singleMapHomologicalComplex F c j).hom.app X).f j =
      F.map (singleObjXSelf c j X).hom ≫ (singleObjXSelf c j (F.obj X)).inv

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_5, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
⊢ ((singleMapHomologicalComplex F c j).hom.app X).f j =
    F.map (singleObjXSelf c j X).hom ≫ (singleObjXSelf c j (F.obj X)).inv

Tactic:
simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

Result:
no goals