harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Basic.lean
theorem sub_lie : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x y : L
m : M
⊢ ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_int_add' [AddCommGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b]
    (f : F) (n : ℤ) (x : G) : f (↑n + x) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
rw [← map_zsmul_add, zsmul_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiff.continuous_deriv (h : ContDiff 𝕜 n f₂) (hn : 1 ≤ n) : Continuous (deriv f₂)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
h : ContDiff 𝕜 n f₂
hn : 1 ≤ n
⊢ Continuous (deriv f₂)

Tactic:
rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl] at hn

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
h : ContDiff 𝕜 n f₂
hn : 0 + 1 ≤ n
⊢ Continuous (deriv f₂)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
h : ContDiff 𝕜 n f₂
hn : 0 + 1 ≤ n
⊢ Continuous (deriv f₂)

Tactic:
exact (contDiff_succ_iff_deriv.mp (h.of_le hn)).2.2.continuous

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedValue_piecewise_const {ι' : Type*} {i j : ι'} {f : ι' → Ω → ℝ} :
    stoppedValue f (s.piecewise (fun _ => i) fun _ => j) = s.piecewise (f i) (f j)

Proof state:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ f (s.piecewise (fun x => i) (fun x => j) ω) ω = s.piecewise (f i) (f j) ω

Tactic:
by_cases hx : ω ∈ s <;> simp [hx]

Result:
no goals

Proof state:
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
⊢ stoppedValue f (s.piecewise (fun x => i) fun x => j) = s.piecewise (f i) (f j)

Tactic:
ext ω

Result:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ stoppedValue f (s.piecewise (fun x => i) fun x => j) ω = s.piecewise (f i) (f j) ω

Proof state:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ stoppedValue f (s.piecewise (fun x => i) fun x => j) ω = s.piecewise (f i) (f j) ω

Tactic:
rw [stoppedValue]

Result:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ f (s.piecewise (fun x => i) (fun x => j) ω) ω = s.piecewise (f i) (f j) ω
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_inf_mul_relrank_of_le (h : A ≤ B) :
    A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_nil (f : α → α) (n) : [].modify f n = []

Proof state:
α : Type u_1
f : α → α
n : Nat
⊢ modify f n [] = []

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x)

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ g (eval₂ f x p) = eval₂ (g.comp f) (g x) p

Tactic:
rw [← eval₂_map, eval₂_at_apply, eval_map]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma RightHomologyData.mapOpcyclesIso_eq [S.HasRightHomology]
    [F.PreservesRightHomologyOf S] :
    S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).pOpcycles ≫ (S.mapOpcyclesIso F).hom =
    (S.map F).pOpcycles ≫ ((hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm).hom

Tactic:
dsimp [mapOpcyclesIso, opcyclesIso]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).pOpcycles ≫ opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) =
    (S.map F).pOpcycles ≫
      opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫
        F.map (opcyclesMap' (𝟙 S) hr S.rightHomologyData)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm

Tactic:
ext

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).pOpcycles ≫ (S.mapOpcyclesIso F).hom =
    (S.map F).pOpcycles ≫ ((hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm).hom

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).pOpcycles ≫ opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) =
    (S.map F).pOpcycles ≫
      opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫
        F.map (opcyclesMap' (𝟙 S) hr S.rightHomologyData)

Tactic:
simp only [map_opcyclesMap', ← opcyclesMap'_comp, Functor.map_id, comp_id,
  Functor.mapShortComplex_obj]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_opow_omega0 : Principal (· ^ ·) ω := fun a b ha hb =>
  match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
    simp_rw [← natCast_opow]
    apply nat_lt_omega0

Proof state:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x1 x2 => x1 ^ x2) ↑m ↑n < ω

Tactic:
simp_rw [← natCast_opow]

Result:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m ^ n) < ω

Proof state:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m ^ n) < ω

Tactic:
apply nat_lt_omega0

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem linearMap_vsub (f : P1 →ᵃ[k] P2) (p1 p2 : P1) : f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p1 p2 : P1
⊢ f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

Tactic:
conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
@[reassoc]
lemma homologySequenceδ_quotient_mapTriangle_obj
    (T : Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (homologyFunctor C (up ℤ) 0).homologySequenceδ
        ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
      (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ (by omega) ≫
        (homologyFunctorFactors C (up ℤ) n₁).inv.app _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
    (homologyFunctorFactors C (up ℤ) n₀).hom.app T.obj₃ ≫
      (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫
        (homologyFunctorFactors C (up ℤ) n₁).inv.app T.obj₁

Tactic:
apply homologyFunctor_shiftMap

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.29, u_1} C
inst✝ : Abelian C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem StrictConcaveOn.ae_eq_const_or_lt_map_average [IsFiniteMeasure μ]
    (hg : StrictConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)
    (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :
    f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ (⨍ x, g (f x) ∂μ) < g (⨍ x, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)

Tactic:
simpa only [Pi.neg_apply, average_neg, neg_lt_neg_iff] using
  hg.neg.ae_eq_const_or_map_average_lt hgc.neg hsc hfs hfi hgi.neg

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsClosed (s i)) :
    IsClosed (⋃ i, s i)

Proof state:
X : Type u
ι : Sort w
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen (s i)ᶜ
⊢ IsOpen (⋂ i, (s i)ᶜ)

Tactic:
exact isOpen_iInter_of_finite h

Result:
no goals

Proof state:
X : Type u
ι : Sort w
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsClosed (s i)
⊢ IsClosed (⋃ i, s i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *

Result:
X : Type u
ι : Sort w
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen (s i)ᶜ
⊢ IsOpen (⋂ i, (s i)ᶜ)
-- Mathlib/Algebra/Group/WithOne/Basic.lean
theorem map_id : map (MulHom.id α) = MonoidHom.id (WithOne α)

Proof state:
case h
α : Type u
inst✝ : Mul α
x : WithOne α
⊢ (map (MulHom.id α)) x = (MonoidHom.id (WithOne α)) x

Tactic:
induction x <;> rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : Mul α
⊢ map (MulHom.id α) = MonoidHom.id (WithOne α)

Tactic:
ext x

Result:
case h
α : Type u
inst✝ : Mul α
x : WithOne α
⊢ (map (MulHom.id α)) x = (MonoidHom.id (WithOne α)) x
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Equiv.tprod_eq_tprod_of_mulSupport {f : β → α} {g : γ → α}
    (e : mulSupport f ≃ mulSupport g) (he : ∀ x, g (e x) = f x) :
    ∏' x, f x = ∏' y, g y :=
  .symm <| tprod_eq_tprod_of_ne_one_bij _ (Subtype.val_injective.comp e.injective) (by simp) he

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
⊢ mulSupport g ⊆ Set.range (Subtype.val ∘ ⇑e)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
lemma ofRootOfUnity_spec {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R)
    {g : Mˣ} (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    ofRootOfUnity hζ hg g = ζ

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
ζ : Rˣ
hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R
g : Mˣ
hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g
⊢ (ofRootOfUnity hζ hg) ↑g = ↑ζ

Tactic:
simp only [ofRootOfUnity, ofUnitHom_eq, equivToUnitHom_symm_coe,
  monoidHomOfForallMemZpowers_apply_gen]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_iff : IsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
⊢ IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
theorem ι_comp_sigmaObjIso_inv (f : α → D ⥤ C) (d : D) (s : α) :
    Sigma.ι (fun s => (f s).obj d) s ≫ (sigmaObjIso f d).inv = (Sigma.ι f s).app d

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasColimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ Sigma.ι (fun s => (f s).obj d) s ≫ (sigmaObjIso f d).inv = (Sigma.ι f s).app d

Tactic:
simp [sigmaObjIso]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparating_unop_iff (𝒢 : Set Cᵒᵖ) : IsCoseparating 𝒢.unop ↔ IsSeparating 𝒢

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set Cᵒᵖ
⊢ IsCoseparating 𝒢.unop ↔ IsSeparating 𝒢

Tactic:
rw [← isSeparating_op_iff, Set.unop_op]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
protected lemma sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Proof state:
case inl
ι : Type u_7
s : Finset ι
f : ι → ℤ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
ι : Type u_7
s✝ : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Tactic:
rw [Int.ediv_mul_cancel (hf _ hs)]

Result:
no goals

Proof state:
case inr
ι : Type u_7
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
rw [Int.ediv_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]

Result:
case inr
ι : Type u_7
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n

Proof state:
case inr
ι : Type u_7
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Result:
case inr
ι : Type u_7
s✝ : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Proof state:
ι : Type u_7
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
ι : Type u_7
s : Finset ι
f : ι → ℤ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

case inr
ι : Type u_7
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
-- Mathlib/Order/CompleteLattice.lean
theorem Function.Surjective.iSup_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
    ⨆ x, g (f x) = ⨆ y, g y

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ ⨆ x, g (f x) = ⨆ y, g y

Tactic:
simp only [iSup.eq_1]

Result:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x => g (f x)) = sSup (range fun y => g y)

Proof state:
case e_a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x => g (f x)) = range fun y => g y

Tactic:
exact hf.range_comp g

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x => g (f x)) = sSup (range fun y => g y)

Tactic:
congr

Result:
case e_a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x => g (f x)) = range fun y => g y
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem Coalgebra.homEquiv_naturality_str_symm (adj : F ⊣ G) (V₁ V₂ : Coalgebra G) (f : V₁ ⟶ V₂) :
    F.map f.f ≫ (adj.homEquiv V₂.V V₂.V).symm V₂.str =
    (adj.homEquiv V₁.V V₁.V).symm V₁.str ≫ f.f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ F.map f.f ≫ (adj.homEquiv V₂.V V₂.V).symm V₂.str = (adj.homEquiv V₁.V V₁.V).symm V₁.str ≫ f.f

Tactic:
rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
  f.h]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem P_idem (q : ℕ) : (P q : K[X] ⟶ K[X]) ≫ P q = P q

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q ≫ P q = P q

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q ≫ P q).f n = (P q).f n

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q ≫ P q).f n = (P q).f n

Tactic:
exact P_f_idem q n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
    Const.get? (Const.alter m k f) k = f (Const.get? m k)

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
⊢ get? (alter m k f) k = f (get? m k)

Tactic:
simp [get?_alter]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} :
    ‖(k : ℤ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k :=
  suffices ‖(k : ℚ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k by
    simpa [norm_intCast_eq_padic_norm]
  padicNormE.norm_int_le_pow_iff_dvd _ _

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
simpa [norm_intCast_eq_padic_norm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem hundred_lt_pow_initialBound_mul {ε : ℝ} (hε : 0 < ε) (l : ℕ) :
    100 < ↑4 ^ initialBound ε l * ε ^ 5

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < ↑7 ⊔ (↑l ⊔ ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

Tactic:
push_cast

Result:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < 7 ⊔ (↑l ⊔ (↑⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 < 4 ^ initialBound ε l * ε ^ 5

Tactic:
rw [← rpow_natCast 4, ← div_lt_iff₀ (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ←
  div_lt_iff₀, initialBound, Nat.cast_max, Nat.cast_max]

Result:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < ↑7 ⊔ (↑l ⊔ ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < 7 ⊔ (↑l ⊔ (↑⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

Tactic:
exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100

Tactic:
norm_num

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

Tactic:
exact log_pos (by norm_num)

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5

Tactic:
exact div_pos (by norm_num) (pow_pos hε 5)

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 1 < 4

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (∀ (a : α), a ∈ m → (l.map Prod.fst).contains a = false) →
      (insertMany m l).size = m.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), a ∈ m → (List.map Prod.fst l).contains a = false) → (insertMany m l).size = m.size + l.length

Tactic:
simp [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), m.contains a = true → (List.map Prod.fst l).contains a = false) →
    (insertMany m l).size = m.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), m.contains a = true → (List.map Prod.fst l).contains a = false) →
    (insertMany m l).size = m.size + l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertMany_list

Result:
no goals
-- Mathlib/Topology/Covering.lean
theorem toTrivialization_apply {x : E} {I : Type*} [TopologicalSpace I]
    (h : IsEvenlyCovered f (f x) I) : (h.toTrivialization x).2 = ⟨x, rfl⟩ :=
  let e := Classical.choose h.2
  let h := Classical.choose_spec h.2
  let he := e.mk_proj_snd' h
  Subtype.ext
    ((e.toPartialEquiv.eq_symm_apply (e.mem_source.mpr h)
            (by rwa [he, e.mem_target, e.coe_fst (e.mem_source.mpr h)])).mpr
        he.symm).symm

Proof state:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
x : E
I : Type u_3
inst✝ : TopologicalSpace I
h✝ : IsEvenlyCovered f (f x) I
e : Trivialization I f := Classical.choose ⋯
h : f x ∈ (Classical.choose ⋯).baseSet := Classical.choose_spec h✝.right
he : (f x, (↑e x).2) = ↑e x := Trivialization.mk_proj_snd' e h
⊢ (f x, (↑e x).2) ∈ e.target

Tactic:
rwa [he, e.mem_target, e.coe_fst (e.mem_source.mpr h)]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[simp, norm_cast] lemma cast_natCast (n : ℕ) : ((n : ℚ≥0) : α) = n

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
simp [cast_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
    l.foldl (fun acc k v => f k v :: acc) acc =
      (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc

Proof state:
α : Type u
β : α → Type v
δ : Type w
l : AssocList α β
acc : List δ
f : (a : α) → β a → δ
⊢ foldl (fun acc k v => f k v :: acc) acc l = (List.map (fun p => f p.fst p.snd) l.toList).reverse ++ acc

Tactic:
induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_modifyKey_self [BEq α] [LawfulBEq α] {k : α} [Inhabited (β k)]
    {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getValueCast! k (modifyKey k f l) = ((getValueCast? k l).map f).get!

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
k : α
inst✝ : Inhabited (β k)
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCast! k (modifyKey k f l) = (Option.map f (getValueCast? k l)).get!

Tactic:
simp [getValueCast!_modifyKey, hl, List.cast_eq_id, List.function_id_comp]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem mulNat_eq_mul (n o) : mulNat o n = o * ofNat n

Proof state:
n : ℕ
o : ONote
⊢ o.mulNat n = o * ↑n

Tactic:
cases o <;> cases n <;> rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_oangle_rev (x y : V) : o.oangle x y + o.oangle y x = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y + o.oangle y x = 0

Tactic:
simp [o.oangle_rev y x]

Result:
no goals