harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
    getKey? (insertManyIfNewUnit m l) k = none

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
not_mem : ¬k ∈ m
contains_eq_false : l.contains k = false
⊢ (insertManyIfNewUnit m l).getKey? k = none

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
contains_eq_false : l.contains k = false
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey? k = none

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
contains_eq_false : l.contains k = false
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey? k = none

Tactic:
exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
  ⟨m.1, _⟩ m.2 not_mem contains_eq_false

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Unitization.lean
theorem uniformity_eq_aux :
    𝓤[instUniformSpaceProd.comap <| addEquiv 𝕜 A] = 𝓤 (Unitization 𝕜 A)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : IsUniformInducing ⇑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)

Tactic:
rw [← key.comap_uniformity]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : IsUniformInducing ⇑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = comap (fun x => ((addEquiv 𝕜 A) x.1, (addEquiv 𝕜 A) x.2)) (𝓤 (𝕜 × A))

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : IsUniformInducing ⇑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = comap (fun x => ((addEquiv 𝕜 A) x.1, (addEquiv 𝕜 A) x.2)) (𝓤 (𝕜 × A))

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)

Tactic:
have key : IsUniformInducing (addEquiv 𝕜 A) :=
  antilipschitzWith_addEquiv.isUniformInducing lipschitzWith_addEquiv.uniformContinuous

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : IsUniformInducing ⇑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_div' : (a / b)⁻¹ = a⁻¹ / b⁻¹

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a / b)⁻¹ = a⁻¹ / b⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a')
    (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) :
    (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

Proof state:
case a.mpr.refine_1.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd ≠ 0

case a.mpr.refine_1.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ ad ≠ 0

case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Tactic:
on_goal 1 => apply div_ne_zero

Result:
case a.mpr.refine_1.ha.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 ≠ 0

case a.mpr.refine_1.ha.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ gcd ≠ 0

case a.mpr.refine_1.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ ad ≠ 0

case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Proof state:
case a.mpr.refine_1.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd ≠ 0

Tactic:
apply div_ne_zero

Result:
case a.mpr.refine_1.ha.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 ≠ 0

case a.mpr.refine_1.ha.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ gcd ≠ 0
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_add_C (c : R) : derivative (X + C c) = 1

Proof state:
R : Type u
inst✝ : Semiring R
c : R
⊢ derivative (X + C c) = 1

Tactic:
rw [derivative_add, derivative_X, derivative_C, add_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem subsingleton_iff : Subsingleton (Subgroup G) ↔ Subsingleton G :=
  ⟨fun _ =>
    ⟨fun x y =>
      have : ∀ i : G, i = 1 := fun i =>
        mem_bot.mp <| Subsingleton.elim (⊤ : Subgroup G) ⊥ ▸ mem_top i
      (this x).trans (this y).symm⟩,
    fun _ => ⟨fun x y => Subgroup.ext fun i => Subsingleton.elim 1 i ▸ by simp [Subgroup.one_mem]⟩⟩

Proof state:
G : Type u_1
inst✝ : Group G
x✝ : Subsingleton G
x y : Subgroup G
i : G
⊢ 1 ∈ x ↔ 1 ∈ y

Tactic:
simp [Subgroup.one_mem]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem linearIndependent_mul_of_flat_right (H : M.LinearDisjoint N) [Module.Flat R N]
    {κ ι : Type*} {m : κ → M} {n : ι → N} (hm : LinearIndependent R m)
    (hn : LinearIndependent R n) : LinearIndependent R fun (i : κ × ι) ↦ (m i.1).1 * (n i.2).1

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)

Tactic:
rw [LinearIndependent] at hm hn ⊢

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i => ↑(m i.1) * ↑(n i.2))

Proof state:
case h.h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
h1 : Function.Injective ⇑i1
h2 : Function.Injective ⇑i2
h : Function.Injective ⇑i
x : κ × ι
⊢ (i ∘ₗ Finsupp.lsingle x) 1 = ((Finsupp.linearCombination R fun i => ↑(m i.1) * ↑(n i.2)) ∘ₗ Finsupp.lsingle x) 1

Tactic:
simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem hasDerivAt_fourier (n : ℤ) (x : ℝ) :
    HasDerivAt (fun y : ℝ => fourier n (y : AddCircle T))
      (2 * π * I * n / T * fourier n (x : AddCircle T)) x

Proof state:
case h.e'_8
T : ℝ
n : ℤ
x : ℝ
⊢ (fun y => 2 * ↑π * I * ↑n * y / ↑T) = fun x => x * (2 * ↑π * I * ↑n / ↑T)

Tactic:
ext1 y

Result:
case h.e'_8.h
T : ℝ
n : ℤ
x : ℝ
y : ℂ
⊢ 2 * ↑π * I * ↑n * y / ↑T = y * (2 * ↑π * I * ↑n / ↑T)

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) ↑x

Tactic:
rw [(fun α β => by ring : ∀ α β : ℂ, α * exp β = exp β * α)]

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * y / ↑T)) (cexp (2 * ↑π * I * ↑n * ↑x / ↑T) * (2 * ↑π * I * ↑n / ↑T)) ↑x

Proof state:
case h.e'_8.h
T : ℝ
n : ℤ
x : ℝ
y : ℂ
⊢ 2 * ↑π * I * ↑n * y / ↑T = y * (2 * ↑π * I * ↑n / ↑T)

Tactic:
ring

Result:
no goals

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * ↑y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) x

Tactic:
refine (?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) ↑x

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => 2 * ↑π * I * ↑n * y / ↑T) (2 * ↑π * I * ↑n / ↑T) ↑x

Tactic:
convert hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1

Result:
case h.e'_8
T : ℝ
n : ℤ
x : ℝ
⊢ (fun y => 2 * ↑π * I * ↑n * y / ↑T) = fun x => x * (2 * ↑π * I * ↑n / ↑T)

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * y / ↑T)) (cexp (2 * ↑π * I * ↑n * ↑x / ↑T) * (2 * ↑π * I * ↑n / ↑T)) ↑x

Tactic:
refine (hasDerivAt_exp _).comp (x : ℂ) ?_

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => 2 * ↑π * I * ↑n * y / ↑T) (2 * ↑π * I * ↑n / ↑T) ↑x

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => (fourier n) ↑y) (2 * ↑π * I * ↑n / ↑T * (fourier n) ↑x) x

Tactic:
simp_rw [fourier_coe_apply]

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * ↑y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) x

Proof state:
T : ℝ
n : ℤ
x : ℝ
α β : ℂ
⊢ α * cexp β = cexp β * α

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertManyIfNewUnit_empty_list
    {l : List α} {k : α} {h} :
    get (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k h = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
h : (insertManyIfNewUnit empty l).val.contains k = true
⊢ get (insertManyIfNewUnit empty l).val k h = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Connected.lean
theorem isPreconnected_sphere (h : 1 < Module.rank ℝ E) (x : E) (r : ℝ) :
    IsPreconnected (sphere x r)

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ IsPreconnected (sphere x r)

Tactic:
exact (isConnected_sphere h x hr).isPreconnected

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
⊢ IsPreconnected (sphere x r)

Tactic:
rcases le_or_lt 0 r with hr|hr

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ IsPreconnected (sphere x r)

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : r < 0
⊢ IsPreconnected (sphere x r)

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : r < 0
⊢ IsPreconnected (sphere x r)

Tactic:
simpa [hr] using isPreconnected_empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsPrefix.head {x y : List α} (h : x <+: y) (hx : x ≠ []) :
    x.head hx = y.head (h.ne_nil hx)

Proof state:
case cons.nil
α : Type u_1
head✝ : α
tail✝ : List α
hx : ¬head✝ :: tail✝ = []
h : head✝ :: tail✝ <+: []
⊢ head✝ = [].head ⋯

case cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
hx : ¬head✝¹ :: tail✝¹ = []
head✝ : α
tail✝ : List α
h : head✝¹ :: tail✝¹ <+: head✝ :: tail✝
⊢ head✝¹ = head✝

Tactic:
all_goals (obtain ⟨_, h⟩ := h; injection h)

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <+: y
hx : x ≠ []
⊢ x.head hx = y.head ⋯

Tactic:
cases x <;> cases y <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢

Result:
case cons.nil
α : Type u_1
head✝ : α
tail✝ : List α
hx : ¬head✝ :: tail✝ = []
h : head✝ :: tail✝ <+: []
⊢ head✝ = [].head ⋯

case cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
hx : ¬head✝¹ :: tail✝¹ = []
head✝ : α
tail✝ : List α
h : head✝¹ :: tail✝¹ <+: head✝ :: tail✝
⊢ head✝¹ = head✝

Proof state:
case cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
hx : ¬head✝¹ :: tail✝¹ = []
head✝ : α
tail✝ : List α
h : head✝¹ :: tail✝¹ <+: head✝ :: tail✝
⊢ head✝¹ = head✝

Tactic:
(obtain ⟨_, h⟩ := h; injection h)

Result:
no goals

Proof state:
case cons.cons.intro
α : Type u_1
head✝¹ : α
tail✝¹ : List α
hx : ¬head✝¹ :: tail✝¹ = []
head✝ : α
tail✝ w✝ : List α
h : head✝¹ :: tail✝¹ ++ w✝ = head✝ :: tail✝
⊢ head✝¹ = head✝

Tactic:
injection h

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
hx : ¬head✝¹ :: tail✝¹ = []
head✝ : α
tail✝ : List α
h : head✝¹ :: tail✝¹ <+: head✝ :: tail✝
⊢ head✝¹ = head✝

Tactic:
obtain ⟨_, h⟩ := h

Result:
case cons.cons.intro
α : Type u_1
head✝¹ : α
tail✝¹ : List α
hx : ¬head✝¹ :: tail✝¹ = []
head✝ : α
tail✝ w✝ : List α
h : head✝¹ :: tail✝¹ ++ w✝ = head✝ :: tail✝
⊢ head✝¹ = head✝
-- Mathlib/Algebra/Group/Pi/Lemmas.lean
theorem Pi.mulSingle_apply_commute [∀ i, MulOneClass <| f i] (x : ∀ i, f i) (i j : I) :
    Commute (mulSingle i (x i)) (mulSingle j (x j))

Proof state:
case inl
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))

Tactic:
rfl

Result:
no goals

Proof state:
case inr
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
exact Pi.mulSingle_commute hij _ _

Result:
no goals

Proof state:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inl
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))

case inr
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
-- Mathlib/Analysis/Seminorm.lean
theorem continuous_of_continuousAt_zero [TopologicalSpace E] [IsTopologicalAddGroup E]
    {p : Seminorm 𝕝 E} (hp : ContinuousAt p 0) : Continuous p

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
this✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ Continuous ⇑p

Tactic:
exact (Seminorm.uniformContinuous_of_continuousAt_zero hp).continuous

Result:
no goals

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
this : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
⊢ Continuous ⇑p

Tactic:
haveI : UniformAddGroup E := uniformAddGroup_of_addCommGroup

Result:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
this✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ Continuous ⇑p

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
⊢ Continuous ⇑p

Tactic:
letI := IsTopologicalAddGroup.toUniformSpace E

Result:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
this : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
⊢ Continuous ⇑p
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@[simp] lemma truncatedSup_singleton (b a : α) : truncatedSup {b} a = if a ≤ b then b else ⊤

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
b a : α
⊢ (if h : a ≤ b then (filter (fun b => a ≤ b) {b}).sup' ⋯ fun x => x else ⊤) = if a ≤ b then b else ⊤

Tactic:
split_ifs <;> simp [Finset.filter_true_of_mem, *]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
b a : α
⊢ {b}.truncatedSup a = if a ≤ b then b else ⊤

Tactic:
simp [truncatedSup]

Result:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
b a : α
⊢ (if h : a ≤ b then (filter (fun b => a ≤ b) {b}).sup' ⋯ fun x => x else ⊤) = if a ≤ b then b else ⊤
-- Mathlib/Topology/Sheaves/Alexandrov.lean
@[simp]
lemma principalOpen_le_iff {x : X} (U : Opens X) :
    principalOpen x ≤ U ↔ x ∈ U

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ ↑(principalOpen x)
⊢ y ∈ ↑U

Tactic:
have := U.isOpen

Result:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ ↑(principalOpen x)
this : IsOpen ↑U
⊢ y ∈ ↑U

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ ↑(principalOpen x)
this : IsUpperSet ↑U
⊢ y ∈ ↑U

Tactic:
exact this hy hx

Result:
no goals

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
⊢ principalOpen x ≤ U ↔ x ∈ U

Tactic:
refine ⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩

Result:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ ↑(principalOpen x)
⊢ y ∈ ↑U

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ ↑(principalOpen x)
this : IsOpen ↑U
⊢ y ∈ ↑U

Tactic:
rw [IsUpperSet.isOpen_iff_isUpperSet] at this

Result:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ ↑(principalOpen x)
this : IsUpperSet ↑U
⊢ y ∈ ↑U
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_Icc_choose (n k : ℕ) : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Proof state:
case inr.succ
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)

Tactic:
rw [← Ico_insert_right (by omega), sum_insert (by simp), Ico_succ_right, ih,
  choose_succ_succ' (n + 1)]

Result:
no goals

Proof state:
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ k ≤ n + 1

Tactic:
omega

Result:
no goals

Proof state:
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ n + 1 ∉ Ico k (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
n k : ℕ
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
rcases lt_or_le n k with h | h

Result:
case inl
n k : ℕ
h : n < k
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Proof state:
case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
induction n, h using le_induction with
| base => simp
| succ n _ ih =>
  rw [← Ico_insert_right (by omega), sum_insert (by simp), Ico_succ_right, ih,
    choose_succ_succ' (n + 1)]

Result:
no goals

Proof state:
n k : ℕ
h : n < k
⊢ n + 1 < k + 1

Tactic:
omega

Result:
no goals

Proof state:
case inl
n k : ℕ
h : n < k
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
rw [choose_eq_zero_of_lt (by omega), Icc_eq_empty_of_lt h, sum_empty]

Result:
no goals

Proof state:
case inr.base
n k : ℕ
⊢ ∑ m ∈ Icc k k, m.choose k = (k + 1).choose (k + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem of_d_ne {i j : α} (h : i ≠ j + 1) : (of X d sq).d i j = 0

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ (of X d sq).d i j = 0

Tactic:
dsimp [of]

Result:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ (if h : i = j + 1 then eqToHom ⋯ ≫ d j else 0) = 0

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ (if h : i = j + 1 then eqToHom ⋯ ≫ d j else 0) = 0

Tactic:
rw [dif_neg h]

Result:
no goals