harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem implicitFunction_apply_image (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
    hf.implicitFunction f f' hf' (f a) 0 = a

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
⊢ implicitFunction f f' hf hf' (f a) 0 = a

Tactic:
haveI := FiniteDimensional.complete 𝕜 F

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
this : CompleteSpace F
⊢ implicitFunction f f' hf hf' (f a) 0 = a

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
this : CompleteSpace F
⊢ implicitFunction f f' hf hf' (f a) 0 = a

Tactic:
apply implicitFunctionOfComplemented_apply_image

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Basic.lean
theorem le_comap_conGen {M N : Type*} [Mul M] [Mul N] (f : M → N)
    (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
    conGen (fun x y ↦ rel (f x) (f y)) ≤ Con.comap f H (conGen rel)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
x y : M
h : (conGen fun x y => rel (f x) (f y)) x y
⊢ (conGen rel) (f x) (f y)

Tactic:
exact .rec (fun x y h ↦ .of (f x) (f y) h) (fun x ↦ .refl (f x))
  (fun _ h ↦ .symm h) (fun _ _ h1 h2 ↦ h1.trans h2) (fun {w x y z} _ _ h1 h2 ↦
  (congrArg (fun a ↦ conGen rel a (f (x * z))) (H w y)).mpr
  (((congrArg (fun a ↦ conGen rel (f w * f y) a) (H x z))).mpr
  (.mul h1 h2))) h

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
x y : M
h : (conGen fun x y => rel (f x) (f y)) x y
⊢ (comap f H (conGen rel)) x y

Tactic:
simp only [Con.comap_rel]

Result:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
x y : M
h : (conGen fun x y => rel (f x) (f y)) x y
⊢ (conGen rel) (f x) (f y)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
⊢ (conGen fun x y => rel (f x) (f y)) ≤ comap f H (conGen rel)

Tactic:
intro x y h

Result:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
x y : M
h : (conGen fun x y => rel (f x) (f y)) x y
⊢ (comap f H (conGen rel)) x y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_left_neg : ∀ a : Int, -a + a = 0
  | 0      => rfl
  | succ m => by simp
  | -[m+1] => by simp

Proof state:
m : Nat
⊢ -↑m.succ + ↑m.succ = 0

Tactic:
simp

Result:
no goals

Proof state:
m : Nat
⊢ - -[m+1] + -[m+1] = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedHull.balanced (s : Set E) : Balanced 𝕜 (balancedHull 𝕜 s)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Tactic:
rw [← smul_assoc] at hx

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ (a • r) • s
⊢ ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Balanced 𝕜 (balancedHull 𝕜 s)

Tactic:
intro a ha

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Tactic:
rintro x ⟨r, hr, hx⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s

Tactic:
simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ (a • r) • s
⊢ ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s

Tactic:
exact ⟨a • r, (SeminormedRing.norm_mul _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem dist_pointReflection_self (x y : P) :
    dist (pointReflection 𝕜 x y) y = ‖(2 : 𝕜)‖ * dist x y

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) y = ‖2‖ * dist x y

Tactic:
rw [dist_pointReflection_self', two_nsmul, ← two_smul 𝕜, norm_smul, ← dist_eq_norm_vsub V]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformlyOn_univ : TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p

Tactic:
simp [TendstoUniformlyOn, TendstoUniformly]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem eq_one_iff_odd {n : ℕ} : (n : ZMod 2) = 1 ↔ Odd n

Proof state:
n : ℕ
⊢ ↑n = 1 ↔ Odd n

Tactic:
rw [← @Nat.cast_one (ZMod 2), ZMod.eq_iff_modEq_nat, Nat.odd_iff, Nat.ModEq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem left_ne_right_of_oangle_ne_zero {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ ≠ 0) : p₁ ≠ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ ≠ p₃

Tactic:
rw [← (vsub_left_injective p₂).ne_iff]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂

Tactic:
exact o.ne_of_oangle_ne_zero h

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bindOnSupport_eq_zero_iff (b : β) :
    p.bindOnSupport f b = 0 ↔ ∀ (a) (ha : p a ≠ 0), f a ha b = 0

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (p.bindOnSupport f) b = 0 ↔ ∀ (a : α) (ha : p a ≠ 0), (f a ha) b = 0

Tactic:
simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]

Result:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (∀ (i : α), ¬p i = 0 → (if h : p i = 0 then 0 else (f i h) b) = 0) ↔ ∀ (a : α) (ha : p a ≠ 0), (f a ha) b = 0

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (∀ (i : α), ¬p i = 0 → (if h : p i = 0 then 0 else (f i h) b) = 0) ↔ ∀ (a : α) (ha : p a ≠ 0), (f a ha) b = 0

Tactic:
exact ⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha),
  fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarMeasure_apply {K₀ : PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
    haarMeasure K₀ s = (haarContent K₀).outerMeasure s / (haarContent K₀).measure K₀

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
s : Set G
hs : MeasurableSet s
⊢ (haarMeasure K₀) s = (haarContent K₀).outerMeasure s / (haarContent K₀).measure ↑K₀

Tactic:
change ((haarContent K₀).measure K₀)⁻¹ * (haarContent K₀).measure s = _

Result:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
s : Set G
hs : MeasurableSet s
⊢ ((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure s =
    (haarContent K₀).outerMeasure s / (haarContent K₀).measure ↑K₀

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
s : Set G
hs : MeasurableSet s
⊢ ((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure s =
    (haarContent K₀).outerMeasure s / (haarContent K₀).measure ↑K₀

Tactic:
simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_zero : round (0 : α) = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ round 0 = 0

Tactic:
simp [round]

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
theorem apply_toDualLeft_symm_apply (f : Dual R N) (x : N) : p (p.toDualLeft.symm f) x = f x

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
f : Dual R N
x : N
h : p (p.toDualLeft.symm f) = f
⊢ (p (p.toDualLeft.symm f)) x = f x

Tactic:
exact congrFun (congrArg DFunLike.coe h) x

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
f : Dual R N
x : N
⊢ (p (p.toDualLeft.symm f)) x = f x

Tactic:
have h := LinearEquiv.apply_symm_apply p.toDualLeft f

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
f : Dual R N
x : N
h : p.toDualLeft (p.toDualLeft.symm f) = f
⊢ (p (p.toDualLeft.symm f)) x = f x

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
f : Dual R N
x : N
h : p.toDualLeft (p.toDualLeft.symm f) = f
⊢ (p (p.toDualLeft.symm f)) x = f x

Tactic:
rw [toDualLeft_apply] at h

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
f : Dual R N
x : N
h : p (p.toDualLeft.symm f) = f
⊢ (p (p.toDualLeft.symm f)) x = f x
-- Mathlib/NumberTheory/Divisors.lean
lemma divisorsAntidiag_natCast (n : ℕ) :
    divisorsAntidiag n =
      (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by
          simp +contextual [disjoint_left, eq_comm]) := rfl

Proof state:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
⊢ Disjoint (map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal)
    (map (negNatCast.prodMap negNatCast) n.divisorsAntidiagonal)

Tactic:
simp +contextual [disjoint_left, eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasSubgroupToLpTrim_right_inv (hm : m ≤ m0) :
    Function.RightInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f) = f

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᶠ[ae (μ.trim hm)] ↑↑f

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᶠ[ae (μ.trim hm)] ↑↑f

Tactic:
refine
  (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᶠ[ae μ] ↑↑f

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᶠ[ae μ] ↑↑f

Tactic:
exact (lpMeasSubgroupToLpTrim_ae_eq hm _).trans (lpTrimToLpMeasSubgroup_ae_eq hm _)

Result:
no goals

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ Function.RightInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)

Tactic:
intro f

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f) = f
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem iSup_induction {ι : Sort*} (p : ι → Submodule R M) {C : M → Prop} {x : M}
    (hx : x ∈ ⨆ i, p i) (hp : ∀ (i), ∀ x ∈ p i, C x) (h0 : C 0)
    (hadd : ∀ x y, C x → C y → C (x + y)) : C x

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : M → Prop
x : M
hx : x ∈ ⨆ i, (p i).toAddSubmonoid
hp : ∀ (i : ι), ∀ x ∈ p i, C x
h0 : C 0
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C x

Tactic:
exact AddSubmonoid.iSup_induction (x := x) _ hx hp h0 hadd

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : M → Prop
x : M
hx : x ∈ ⨆ i, p i
hp : ∀ (i : ι), ∀ x ∈ p i, C x
h0 : C 0
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C x

Tactic:
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
C : M → Prop
x : M
hx : x ∈ ⨆ i, (p i).toAddSubmonoid
hp : ∀ (i : ι), ∀ x ∈ p i, C x
h0 : C 0
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C x
-- Mathlib/Algebra/Group/EvenFunction.lean
/-- An odd function vanishes at zero. -/
lemma Odd.map_zero [NegZeroClass α] (hf : f.Odd) : f 0 = 0

Proof state:
α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : NoZeroSMulDivisors ℕ β
f : α → β
inst✝ : NegZeroClass α
hf : Function.Odd f
⊢ f 0 = 0

Tactic:
simp only [← neg_eq_self ℕ, ← hf 0, neg_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_comp_one_sub_X (p : R[X]) :
    derivative (p.comp (1 - X)) = -p.derivative.comp (1 - X)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ derivative (p.comp (1 - X)) = -(derivative p).comp (1 - X)

Tactic:
simp [derivative_comp]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem card_eq_zero {s : Multiset α} : card s = 0 ↔ s = 0 :=
  ⟨fun h => (eq_of_le_of_card_le (zero_le _) (le_of_eq h)).symm, fun e => by simp [e]⟩

Proof state:
α : Type u_1
s : Multiset α
e : s = 0
⊢ s.card = 0

Tactic:
simp [e]

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem wellFoundedGT_iff_monotone_chain_condition [PartialOrder α] :
    WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m :=
  wellFoundedGT_iff_monotone_chain_condition'.trans <| by
  congrm ∀ a, ∃ n, ∀ m h, ?_
  rw [lt_iff_le_and_ne]
  simp [a.mono h]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
⊢ (∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
congrm ∀ a, ∃ n, ∀ m h, ?_

Result:
case a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬a n < a m ↔ a n = a m

Proof state:
case a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬(a n ≤ a m ∧ a n ≠ a m) ↔ a n = a m

Tactic:
simp [a.mono h]

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬a n < a m ↔ a n = a m

Tactic:
rw [lt_iff_le_and_ne]

Result:
case a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬(a n ≤ a m ∧ a n ≠ a m) ↔ a n = a m
-- Mathlib/Order/Filter/AtTopBot/Defs.lean
theorem Antitone.piecewise_eventually_eq_iInter {β : α → Type*} [Preorder ι] {s : ι → Set α}
    [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋂ i, s i)]
    (hs : Antitone s) (f g : (a : α) → β a) (a : α) :
    ∀ᶠ i in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a

Proof state:
case h.e'_2.h.h.e'_2
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ i, s i
hs : Antitone s
f g : (a : α) → β a
a : α
x✝ : ι
⊢ ((compl ∘ s) x✝).piecewise g f a = (s x✝).piecewise f g a

Tactic:
convert congr_fun (Set.piecewise_compl (s _) g f) a

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ i, s i
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a

Tactic:
convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3

Result:
case h.e'_2.h.h.e'_2
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ i, s i
hs : Antitone s
f g : (a : α) → β a
a : α
x✝ : ι
⊢ ((compl ∘ s) x✝).piecewise g f a = (s x✝).piecewise f g a

case h.e'_2.h.h.e'_3
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ i, s i
hs : Antitone s
f g : (a : α) → β a
a : α
x✝ : ι
⊢ (⋃ i, (compl ∘ s) i).piecewise g f a = (⋂ i, s i).piecewise f g a
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem cauchySeq_of_dist_le_of_summable (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
    (hd : Summable d) : CauchySeq f

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
⊢ CauchySeq f

Tactic:
lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)

Result:
case intro
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => ↑(d i)
⊢ CauchySeq f

Proof state:
case intro.hf
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => ↑(d i)
⊢ ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)

Tactic:
exact_mod_cast hf

Result:
no goals

Proof state:
case intro.hd
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => ↑(d i)
⊢ Summable d

Tactic:
exact_mod_cast hd

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => ↑(d i)
⊢ CauchySeq f

Tactic:
apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)

Result:
case intro.hf
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => ↑(d i)
⊢ ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)

case intro.hd
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => ↑(d i)
⊢ Summable d
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem padicNorm_p (hp : 1 < p) : padicNorm p p = (p : ℚ)⁻¹

Proof state:
p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p = (↑p)⁻¹

Tactic:
simp [padicNorm, (pos_of_gt hp).ne', padicValNat.self hp]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem to_nat_inj {m n : PosNum} : (m : ℕ) = n ↔ m = n :=
  ⟨fun h => Num.pos.inj <| by rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h], congr_arg _⟩

Proof state:
m n : PosNum
h : ↑m = ↑n
⊢ pos m = pos n

Tactic:
rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]

Result:
no goals