harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_apply_c : seminormFromConst' hf1 hc hpm c = f c :=
  have hlim : Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ seminormFromConst_seq c f c = fun _n => f c

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
⊢ seminormFromConst_seq c f c n = f c

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hseq : seminormFromConst_seq c f c = fun _n => f c
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))

Tactic:
rw [hseq]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hseq : seminormFromConst_seq c f c = fun _n => f c
⊢ Tendsto (fun _n => f c) atTop (𝓝 (f c))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hseq : seminormFromConst_seq c f c = fun _n => f c
⊢ Tendsto (fun _n => f c) atTop (𝓝 (f c))

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))

Tactic:
have hseq : seminormFromConst_seq c f c = fun _n ↦ f c := by
  ext n
  simp only [seminormFromConst_seq]
  rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm,  mul_div_assoc,
    div_self (pow_ne_zero n hc), mul_one]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hseq : seminormFromConst_seq c f c = fun _n => f c
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
⊢ seminormFromConst_seq c f c n = f c

Tactic:
simp only [seminormFromConst_seq]

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
⊢ f (c * c ^ n) / f c ^ n = f c

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
⊢ f (c * c ^ n) / f c ^ n = f c

Tactic:
rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm,  mul_div_assoc,
  div_self (pow_ne_zero n hc), mul_one]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem snd_apply' (κ : Kernel α (β × γ)) (a : α) {s : Set γ} (hs : MeasurableSet s) :
    snd κ a s = κ a {p | p.2 ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ a) (Prod.snd ⁻¹' s) = (κ a) {p | p.2 ∈ s}

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ.snd a) s = (κ a) {p | p.2 ∈ s}

Tactic:
rw [snd_apply, Measure.map_apply measurable_snd hs]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ a) (Prod.snd ⁻¹' s) = (κ a) {p | p.2 ∈ s}
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
/-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`. -/
lemma apply_nat_le_self (n : ℕ) : abv n ≤ n

Proof state:
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
n : ℕ
⊢ abv ↑n ≤ ↑n

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
n : ℕ
h✝ : Subsingleton R
⊢ abv ↑n ≤ ↑n

case inr
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
n : ℕ
h✝ : Nontrivial R
⊢ abv ↑n ≤ ↑n

Proof state:
case inr.succ
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
h✝ : Nontrivial R
n : ℕ
hn : abv ↑n ≤ ↑n
⊢ abv ↑(n + 1) ≤ ↑(n + 1)

Tactic:
simp only [Nat.cast_succ]

Result:
case inr.succ
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
h✝ : Nontrivial R
n : ℕ
hn : abv ↑n ≤ ↑n
⊢ abv (↑n + 1) ≤ ↑n + 1

Proof state:
case inr.zero
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
h✝ : Nontrivial R
⊢ abv ↑0 ≤ ↑0

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : OrderedRing S
abv : AbsoluteValue R S
inst✝ : IsDomain S
n : ℕ
h✝ : Subsingleton R
⊢ abv ↑n ≤ ↑n

Tactic:
simp [Subsingleton.eq_zero (n : R)]

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
lemma quotient_mk_sInf_eq {S : Set (Setoid α)} {x y : α} :
    Quotient.mk (sInf S) x = Quotient.mk (sInf S) y ↔ ∀ s ∈ S, s x y

Proof state:
α : Type u_1
S : Set (Setoid α)
x y : α
⊢ ⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, s x y

Tactic:
simp [sInf_iff]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem finrank_adjoin_simple_eq_one_iff :
    finrank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

Tactic:
rw [finrank_adjoin_eq_one_iff]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ {α} ⊆ ↑⊥ ↔ α ∈ ⊥

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ {α} ⊆ ↑⊥ ↔ α ∈ ⊥

Tactic:
exact Set.singleton_subset_iff

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalAverage.lean
theorem interval_average_eq (f : ℝ → E) (a b : ℝ) :
    (⨍ x in a..b, f x) = (b - a)⁻¹ • ∫ x in a..b, f x

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_Ioc, intervalIntegral.integral_of_ge h.le,
  ENNReal.toReal_ofReal (sub_nonneg.2 h.le), smul_neg, ← neg_smul, ← inv_neg, neg_sub]

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
rw [setAverage_eq, uIoc_of_le h, Real.volume_Ioc, intervalIntegral.integral_of_le h,
  ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
rcases le_or_lt a b with h | h

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_same {a : α} {f : α →₀ M} : (f.erase a) a = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
⊢ (erase a f) a = 0

Tactic:
simp only [erase, coe_mk, ite_true]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
⊢ (erase a f) a = 0

Tactic:
classical simp only [erase, coe_mk, ite_true]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_cthickening_subset (ε : ℝ) (hδ : 0 ≤ δ) (s : Set α) :
    thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Proof state:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact infEdist_le_edist_add_infEdist.trans_lt
  (ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s

Tactic:
simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEdist_lt_iff,
  ENNReal.ofReal_add hε hδ]

Result:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEdist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Tactic:
intro x

Result:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Tactic:
obtain hε | hε := le_total ε 0

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hε, empty_subset]

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEdist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
rintro ⟨y, hy, hxy⟩

Result:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_nonneg (I : FractionalIdeal R⁰ K) : 0 ≤ absNorm I

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
⊢ 0 ≤ absNorm I

Tactic:
dsimp [absNorm]

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
⊢ 0 ≤ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
⊢ 0 ≤ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
positivity

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueSet_map_of_equiv (G : SimpleGraph α) (e : α ≃ β) (n : ℕ) :
    (G.map e.toEmbedding).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Proof state:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet 1 = map e.toEmbedding '' G.cliqueSet 1

Tactic:
ext

Result:
case inl.h
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
x✝ : Finset β
⊢ x✝ ∈ (SimpleGraph.map e.toEmbedding G).cliqueSet 1 ↔ x✝ ∈ map e.toEmbedding '' G.cliqueSet 1

Proof state:
case inl.h
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
x✝ : Finset β
⊢ x✝ ∈ (SimpleGraph.map e.toEmbedding G).cliqueSet 1 ↔ x✝ ∈ map e.toEmbedding '' G.cliqueSet 1

Tactic:
simp [e.exists_congr_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
obtain rfl | hn := eq_or_ne n 1

Result:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet 1 = map e.toEmbedding '' G.cliqueSet 1

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
exact cliqueSet_map hn _ _

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem eq_orthogonalProjection_of_eq_submodule {K' : Submodule 𝕜 E} [HasOrthogonalProjection K']
    (h : K = K') (u : E) : (orthogonalProjection K u : E) = (orthogonalProjection K' u : E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection K
K' : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K'
h : K = K'
u : E
⊢ ↑((orthogonalProjection K) u) = ↑((orthogonalProjection K') u)

Tactic:
subst h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection K
u : E
inst✝ : HasOrthogonalProjection K
⊢ ↑((orthogonalProjection K) u) = ↑((orthogonalProjection K) u)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection K
u : E
inst✝ : HasOrthogonalProjection K
⊢ ↑((orthogonalProjection K) u) = ↑((orthogonalProjection K) u)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleMap_eq_center_iff {c : ℂ} {R : ℝ} {θ : ℝ} : circleMap c R θ = c ↔ R = 0

Proof state:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ = c ↔ R = 0

Tactic:
simp [circleMap, exp_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.unwrap_isNeutral
  {ctx : Context α}
  {x : Nat}
  : ContextInformation.isNeutral ctx x = true → LawfulIdentity (EvalInformation.evalOp ctx) (EvalInformation.evalVar (β := α) ctx x)

Proof state:
α : Sort u_1
ctx : Context α
x : Nat
a✝ :
  (match none with
    | some val => true
    | none => false) =
    true
⊢ LawfulIdentity ctx.op (ctx.var x).value

Tactic:
contradiction

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
x : Nat
hn : PLift (LawfulIdentity ctx.op (ctx.var x).value)
⊢ (match some hn with
      | some val => true
      | none => false) =
      true →
    LawfulIdentity ctx.op (ctx.var x).value

Tactic:
intro

Result:
α : Sort u_1
ctx : Context α
x : Nat
hn : PLift (LawfulIdentity ctx.op (ctx.var x).value)
a✝ :
  (match some hn with
    | some val => true
    | none => false) =
    true
⊢ LawfulIdentity ctx.op (ctx.var x).value

Proof state:
α : Sort u_1
ctx : Context α
x : Nat
⊢ (match none with
      | some val => true
      | none => false) =
      true →
    LawfulIdentity ctx.op (ctx.var x).value

Tactic:
intro

Result:
α : Sort u_1
ctx : Context α
x : Nat
a✝ :
  (match none with
    | some val => true
    | none => false) =
    true
⊢ LawfulIdentity ctx.op (ctx.var x).value

Proof state:
α : Sort u_1
ctx : Context α
x : Nat
hn : PLift (LawfulIdentity ctx.op (ctx.var x).value)
a✝ :
  (match some hn with
    | some val => true
    | none => false) =
    true
⊢ LawfulIdentity ctx.op (ctx.var x).value

Tactic:
exact hn.down

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
x : Nat
⊢ (match (ctx.var x).neutral with
      | some val => true
      | none => false) =
      true →
    LawfulIdentity ctx.op (ctx.var x).value

Tactic:
match (var ctx x).neutral with
| some hn =>
  intro
  exact hn.down
| none => intro; contradiction

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
x : Nat
⊢ ContextInformation.isNeutral ctx x = true →
    LawfulIdentity (EvalInformation.evalOp ctx) (EvalInformation.evalVar ctx x)

Tactic:
simp [ContextInformation.isNeutral, Option.isSome, EvalInformation.evalOp, EvalInformation.evalVar]

Result:
α : Sort u_1
ctx : Context α
x : Nat
⊢ (match (ctx.var x).neutral with
      | some val => true
      | none => false) =
      true →
    LawfulIdentity ctx.op (ctx.var x).value
-- Mathlib/Computability/PostTuringMachine.lean
theorem stmts₁_self {q : Stmt Γ Λ σ} : q ∈ stmts₁ q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ q

Tactic:
cases q <;> simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem exists_lt_omega0_opow' {α} {o b : Ordinal} (hb : 1 < b) (ho : o.IsLimit)
    {f : α → Ordinal} (H : ∀ ⦃a⦄, a < o → ∃ i, a < f i) ⦃a⦄ (h : a < b ^ o) :
        ∃ i, a < b ^ f i

Proof state:
case intro.intro
α : Sort u_1
o b : Ordinal.{u_2}
hb : 1 < b
ho : o.IsLimit
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
a : Ordinal.{u_2}
h : a < b ^ o
d : Ordinal.{u_2}
hd : d < o
h' : a < b ^ d
⊢ ∃ i, a < b ^ f i

Tactic:
exact (H hd).imp fun i hi => h'.trans <| (opow_lt_opow_iff_right hb).2 hi

Result:
no goals

Proof state:
α : Sort u_1
o b : Ordinal.{u_2}
hb : 1 < b
ho : o.IsLimit
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
a : Ordinal.{u_2}
h : a < b ^ o
⊢ ∃ i, a < b ^ f i

Tactic:
obtain ⟨d, hd, h'⟩ := (lt_opow_of_limit (zero_lt_one.trans hb).ne' ho).1 h

Result:
case intro.intro
α : Sort u_1
o b : Ordinal.{u_2}
hb : 1 < b
ho : o.IsLimit
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
a : Ordinal.{u_2}
h : a < b ^ o
d : Ordinal.{u_2}
hd : d < o
h' : a < b ^ d
⊢ ∃ i, a < b ^ f i
-- Mathlib/Data/Finset/Card.lean
theorem card_union_add_card_inter (s t : Finset α) :
    #(s ∪ t) + #(s ∩ t) = #s + #t :=
  Finset.induction_on t (by simp) fun a r har h => by by_cases a ∈ s <;>
    simp [*, ← Nat.add_assoc, Nat.add_right_comm _ 1]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ ∅) + #(s ∩ ∅) = #s + #∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : a ∉ r
h : #(s ∪ r) + #(s ∩ r) = #s + #r
⊢ #(s ∪ insert a r) + #(s ∩ insert a r) = #s + #(insert a r)

Tactic:
by_cases a ∈ s <;>
simp [*, ← Nat.add_assoc, Nat.add_right_comm _ 1]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_diff [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s \ t).Finite) : h.toFinset = hs.toFinset \ ht.toFinset

Proof state:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
⊢ h.toFinset = hs.toFinset \ ht.toFinset

Tactic:
ext

Result:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset \ ht.toFinset

Proof state:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset \ ht.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Matrix.lean
theorem uniformContinuous {β : Type*} [UniformSpace β] {f : β → Matrix m n 𝕜} :
    UniformContinuous f ↔ ∀ i j, UniformContinuous fun x => f x i j

Proof state:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a => (a.1 i i_1, a.2 i i_1)) ∘ fun x => (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)

Tactic:
apply Iff.intro <;> intro a <;> apply a

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j

Tactic:
simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]

Result:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a => (a.1 i i_1, a.2 i i_1)) ∘ fun x => (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
-- Mathlib/Data/List/GetD.lean
theorem getElem?_getD_singleton_default_eq (n : ℕ) : [d][n]?.getD d = d

Proof state:
α : Type u
d : α
n : ℕ
⊢ [d][n]?.getD d = d

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Order.lean
theorem order_pow {f : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) {n : ℕ} :
    (hf.pow n).order = n • hf.order

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
hn : ⋯.order = n • hf.order
⊢ ⋯.order = (n + 1) • hf.order

Tactic:
simp [add_mul, pow_add, (hf.pow n).order_mul hf, hn]

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ ⋯.order = 0 • hf.order

case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
n✝ : ℕ
a✝ : ⋯.order = n✝ • hf.order
⊢ ⋯.order = (n✝ + 1) • hf.order

Tactic:
case zero =>
  simp [AnalyticAt.order_eq_zero_iff]

Result:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
n✝ : ℕ
a✝ : ⋯.order = n✝ • hf.order
⊢ ⋯.order = (n✝ + 1) • hf.order

Proof state:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
n✝ : ℕ
a✝ : ⋯.order = n✝ • hf.order
⊢ ⋯.order = (n✝ + 1) • hf.order

Tactic:
case succ n hn =>
  simp [add_mul, pow_add, (hf.pow n).order_mul hf, hn]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ ⋯.order = 0 • hf.order

Tactic:
simp [AnalyticAt.order_eq_zero_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ ⋯.order = n • hf.order

Tactic:
induction n

Result:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ ⋯.order = 0 • hf.order

case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
n✝ : ℕ
a✝ : ⋯.order = n✝ • hf.order
⊢ ⋯.order = (n✝ + 1) • hf.order
-- Mathlib/Algebra/Group/Semiconj/Units.lean
@[to_additive (attr := simp)]
lemma units_zpow_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) :
    ∀ m : ℤ, SemiconjBy a ↑(x ^ m) ↑(y ^ m)
  | (n : ℕ) => by simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]
  | -[n+1] => by simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ ↑n) ↑(y ^ ↑n)

Tactic:
simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])

Tactic:
simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma tendsto_rightDeriv_klFun_atTop :
    Tendsto (fun x ↦ derivWithin klFun (Ioi x) x) atTop atTop

Proof state:
⊢ Tendsto (fun x => log x) atTop atTop

Tactic:
exact tendsto_log_atTop

Result:
no goals

Proof state:
⊢ Tendsto (fun x => derivWithin klFun (Ioi x) x) atTop atTop

Tactic:
simp only [rightDeriv_klFun]

Result:
⊢ Tendsto (fun x => log x) atTop atTop