harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_append_1 (s m n : Nat) :
    range' s m ++ range' (s + m) n = range' s (m + n)

Proof state:
s m n : Nat
⊢ range' s m ++ range' (s + m) n = range' s (m + n)

Tactic:
simpa using range'_append s m n 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_append_left {l₁ l₂ : List α} (h : l₁ ≠ []) :
    head (l₁ ++ l₂) (fun h => by simp_all) = head l₁ h

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ ≠ []
⊢ ¬l₁.isEmpty = true

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ ≠ []
⊢ (l₁ ++ l₂).head ⋯ = l₁.head h

Tactic:
rw [head_append, dif_neg (by simp_all)]

Result:
no goals

Proof state:
α : Type ?u.201720
l₁ l₂ : List α
h✝ : l₁ ≠ []
h : l₁ ++ l₂ = []
⊢ False

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem eq_of_mul_eq_mul_right {a b c : Int} (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
  have : (b - c) * a = 0

Proof state:
a b c : Int
ha : a ≠ 0
h : b * a = c * a
⊢ (b - c) * a = 0

Tactic:
rwa [Int.sub_mul, Int.sub_eq_zero]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma predAbove_zero_succ [NeZero n] {i : Fin n} : predAbove 0 i.succ = i

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ predAbove 0 i.succ = i

Tactic:
rw [predAbove_succ_of_le _ _ (Fin.zero_le' _)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma in₂₀_iff' :
    (graph t).Adj (in₂ c) (in₀ a) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.2.2 = c ∧ x.1 = a where
  mp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
⊢ (∃ x ∈ t, x.2.2 = c ∧ x.1 = a) → (graph t).Adj (in₂ c) (in₀ a)

Tactic:
rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩

Result:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₀ (a, b, c).1)

Proof state:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₀ (a, b, c).1)

Tactic:
constructor

Result:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, ?intro.mk.mk.intro.intro.b, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ β

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ (a, b✝, c).2.2 = c ∧ (a, b✝, c).1 = a

Tactic:
simp

Result:
no goals

Proof state:
case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a

Tactic:
exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, ?intro.mk.mk.intro.intro.b, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ β

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
⊢ (graph t).Adj (in₂ c) (in₀ a) → ∃ x ∈ t, x.2.2 = c ∧ x.1 = a

Tactic:
rintro ⟨⟩

Result:
case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem add_eq_max_of_ne {F α : Type*} [AddGroup α] [FunLike F α ℝ]
    [AddGroupSeminormClass F α ℝ] {f : F} (hna : IsNonarchimedean f) {x y : α} (hne : f x ≠ f y) :
    f (x + y) = max (f x) (f y)

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
⊢ f (x + y) = f x ⊔ f y

Tactic:
let _ := AddGroupSeminormClass.toSeminormedAddGroup f

Result:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
⊢ f (x + y) = f x ⊔ f y

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
⊢ f (x + y) = f x ⊔ f y

Tactic:
have := AddGroupSeminormClass.isUltrametricDist hna

Result:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ f (x + y) = f x ⊔ f y

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ f (x + y) = f x ⊔ f y

Tactic:
simp only [← AddGroupSeminormClass.toSeminormedAddGroup_norm_eq] at hne ⊢

Result:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : ‖x‖ ≠ ‖y‖
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ ‖x + y‖ = ‖x‖ ⊔ ‖y‖

Proof state:
F : Type u_1
α : Type u_2
inst✝² : AddGroup α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : ‖x‖ ≠ ‖y‖
x✝ : SeminormedAddGroup α := AddGroupSeminormClass.toSeminormedAddGroup f
this : IsUltrametricDist α
⊢ ‖x + y‖ = ‖x‖ ⊔ ‖y‖

Tactic:
exact norm_add_eq_max_of_norm_ne_norm hne

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_div_mul_right (a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) :
    a * c / (b * c) = a / b

Proof state:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ⊤
⊢ a * c / (b * c) = a / b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
  ENNReal.mul_inv_cancel hc hc', mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic [CompleteSpace E]
    (hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Iic a)) :
    Tendsto f atBot (𝓝 (limUnder atBot f))

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Tactic:
have L : Tendsto g atTop (𝓝 (limUnder atTop g)) := by
  apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg
  exact ((MeasurePreserving.integrableOn_comp_preimage (Measure.measurePreserving_neg _)
    (Homeomorph.neg ℝ).measurableEmbedding).2 f'int.neg).mono_set (by simp)

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ IntegrableOn (fun x => -f' (-x)) (Ioi (-a)) volume

Tactic:
exact ((MeasurePreserving.integrableOn_comp_preimage (Measure.measurePreserving_neg _)
  (Homeomorph.neg ℝ).measurableEmbedding).2 f'int.neg).mono_set (by simp)

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem prod {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith Kf f s)
    (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf ⊔ Kg) (fun x => (f x, g x)) s

Tactic:
intro _ hx _ hy

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x => (f x, g x)) x✝) ((fun x => (f x, g x)) y✝) ≤ ↑(Kf ⊔ Kg) * edist x✝ y✝

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x => (f x, g x)) x✝).1 ((fun x => (f x, g x)) y✝).1 ⊔
      edist ((fun x => (f x, g x)) x✝).2 ((fun x => (f x, g x)) y✝).2 ≤
    ↑Kf * edist x✝ y✝ ⊔ ↑Kg * edist x✝ y✝

Tactic:
exact max_le_max (hf hx hy) (hg hx hy)

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x => (f x, g x)) x✝) ((fun x => (f x, g x)) y✝) ≤ ↑(Kf ⊔ Kg) * edist x✝ y✝

Tactic:
rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x => (f x, g x)) x✝).1 ((fun x => (f x, g x)) y✝).1 ⊔
      edist ((fun x => (f x, g x)) x✝).2 ((fun x => (f x, g x)) y✝).2 ≤
    ↑Kf * edist x✝ y✝ ⊔ ↑Kg * edist x✝ y✝
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comapFunIsLocallyFraction (f : R →+* S) (U : Opens (PrimeSpectrum.Top R))
    (V : Opens (PrimeSpectrum.Top S)) (hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1)
    (s : ∀ x : U, Localizations R x) (hs : (isLocallyFraction R).toPrelocalPredicate.pred s) :
    (isLocallyFraction S).toPrelocalPredicate.pred (comapFun f U V hUV s)

Proof state:
case mk
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
⊢ ∃ V_1, ∃ (_ : ↑⟨p, hpV⟩ ∈ V_1), ∃ i, (isFractionPrelocal S).pred fun x => comapFun f U V hUV s (i x)

Tactic:
rcases hs ⟨PrimeSpectrum.comap f p, hUV hpV⟩ with ⟨W, m, iWU, a, b, h_frac⟩

Result:
case mk.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
h_frac :
  ∀ (x : ↥W),
    b ∉ (↑x).asIdeal ∧
      (fun x => s (iWU x)) x * (algebraMap R (Localizations R ↑x)) b = (algebraMap R (Localizations R ↑x)) a
⊢ ∃ V_1, ∃ (_ : ↑⟨p, hpV⟩ ∈ V_1), ∃ i, (isFractionPrelocal S).pred fun x => comapFun f U V hUV s (i x)

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
⊢ (isLocallyFraction S).pred (comapFun f U V hUV s)

Tactic:
rintro ⟨p, hpV⟩

Result:
case mk
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
⊢ ∃ V_1, ∃ (_ : ↑⟨p, hpV⟩ ∈ V_1), ∃ i, (isFractionPrelocal S).pred fun x => comapFun f U V hUV s (i x)
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma ker_polarization_eq_ker_rootForm :
    LinearMap.ker P.Polarization = LinearMap.ker P.RootForm

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ LinearMap.ker P.Polarization = LinearMap.ker P.RootForm

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x✝ : M
⊢ x✝ ∈ LinearMap.ker P.Polarization ↔ x✝ ∈ LinearMap.ker P.RootForm

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x✝ : M
⊢ x✝ ∈ LinearMap.ker P.Polarization ↔ x✝ ∈ LinearMap.ker P.RootForm

Tactic:
simp only [LinearMap.mem_ker, P.polarization_apply_eq_zero_iff]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_pos : ∀ {n k}, k ≤ n → 0 < choose n k
  | 0, _, hk => by rw [Nat.eq_zero_of_le_zero hk]; decide
  | n + 1, 0, _ => by simp
  | _ + 1, _ + 1, hk => Nat.add_pos_left (choose_pos (le_of_succ_le_succ hk)) _

Proof state:
n : ℕ
x✝ : 0 ≤ n + 1
⊢ 0 < (n + 1).choose 0

Tactic:
simp

Result:
no goals

Proof state:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝

Tactic:
rw [Nat.eq_zero_of_le_zero hk]

Result:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0

Proof state:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem nonempty_of_pos_sInf {s : Set ℕ} (h : 0 < sInf s) : s.Nonempty

Proof state:
s : Set ℕ
h : 0 < sInf s
contra : ¬s.Nonempty
⊢ False

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at contra

Result:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False

Proof state:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False

Tactic:
have h' : sInf s ≠ 0 := ne_of_gt h

Result:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False

Proof state:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅

Tactic:
right

Result:
case h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅

Proof state:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0

Tactic:
rw [Nat.sInf_eq_zero]

Result:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅

Proof state:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False

Tactic:
apply h'

Result:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0

Proof state:
case h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅

Tactic:
assumption

Result:
no goals

Proof state:
s : Set ℕ
h : 0 < sInf s
⊢ s.Nonempty

Tactic:
by_contra contra

Result:
s : Set ℕ
h : 0 < sInf s
contra : ¬s.Nonempty
⊢ False
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) :
    μ (closedBall x r) = μ (closedBall (0 : E) r)

Proof state:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ closedBall 0 r = (fun x_1 => x + x_1) ⁻¹' closedBall x r

Tactic:
simp [preimage_add_closedBall]

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : closedBall 0 r = (fun x_1 => x + x_1) ⁻¹' closedBall x r
⊢ μ (closedBall x r) = μ (closedBall 0 r)

Tactic:
rw [this, measure_preimage_add]

Result:
no goals
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem IsPreconnected.eqOn_const_of_mapsTo {S : Set α} (hS : IsPreconnected S)
    {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S)
    (hTm : MapsTo f S T) (hne : T.Nonempty) : ∃ y ∈ T, EqOn f (const α y) S

Proof state:
case inl
α : Type u
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hne : T.Nonempty
hS : IsPreconnected ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y ∈ T, EqOn f (const α y) ∅

Tactic:
exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩

Result:
no goals

Proof state:
case inr.intro
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hc hTm hx' hx⟩

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)

Result:
case inl
α : Type u
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hne : T.Nonempty
hS : IsPreconnected ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y ∈ T, EqOn f (const α y) ∅

case inr.intro
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range_succ_eq_map (n : Nat) : range (n + 1) =
    (#v[0] ++ map succ (range n)).cast (by omega)

Proof state:
n : Nat
⊢ range (n + 1) = Vector.cast ⋯ ({ toArray := #[0], size_toArray := ⋯ } ++ map succ (range n))

Tactic:
rw [← toArray_inj]

Result:
n : Nat
⊢ (range (n + 1)).toArray = (Vector.cast ⋯ ({ toArray := #[0], size_toArray := ⋯ } ++ map succ (range n))).toArray

Proof state:
n : Nat
⊢ (range (n + 1)).toArray = (Vector.cast ⋯ ({ toArray := #[0], size_toArray := ⋯ } ++ map succ (range n))).toArray

Tactic:
simp [Array.range_succ_eq_map]

Result:
no goals

Proof state:
n : Nat
⊢ 1 + n = n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem mul_add_mul : a * b + b * a = 0

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0

Tactic:
rwa [self_eq_add_right] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * b + (b * a + b * b) = a + a * b + (b * a + b)

Tactic:
simp only [mul_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0

Tactic:
have : a + b = a + b + (a * b + b * a) :=
  calc
    a + b = (a + b) * (a + b) := by rw [mul_self]
    _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
    _ = a + a * b + (b * a + b) := by simp only [mul_self]
    _ = a + b + (a * b + b * a) := by abel

Result:
α : Type u_1
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)

Tactic:
rw [add_mul, mul_add, mul_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + b = (a + b) * (a + b)

Tactic:
rw [mul_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)

Tactic:
abel

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem div_of_dvd (h : b ∣ a) :
    padicValNat p (a / b) = padicValNat p a - padicValNat p b

Proof state:
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b

case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Proof state:
case inr.intro.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b

Tactic:
rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]

Result:
no goals

Proof state:
case inr.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b

Tactic:
obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha

Result:
case inr.intro.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b

Proof state:
case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b

Tactic:
simp

Result:
no goals

Proof state:
case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case inr.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem rightAdjointUniq_hom_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
    whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x✝ : D
⊢ (whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit).app x✝ = adj1.counit.app x✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit = adj1.counit

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x✝ : D
⊢ (whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit).app x✝ = adj1.counit.app x✝