harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {s : Sphere P}
    {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃)
    (hp₂p₃ : p₂ ≠ p₃) :
    ((Real.Angle.tan (∡ p₁ p₂ p₃))⁻¹ / 2) • o.rotation (π / 2 : ℝ) (p₃ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₃ =
      s.center

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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ ((∡ p₁ p₂ p₃).tan⁻¹ / 2) • («o».rotation ↑(π / 2)) (p₃ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₃ = s.center

Tactic:
convert tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₃ hp₁p₃

Result:
case h.e'_2.h.e'_5.h.e'_5.h.e'_5
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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ (∡ p₁ p₂ p₃).tan⁻¹ = (∡ p₃ p₁ s.center).tan

Proof state:
case h.e'_2.h.e'_5.h.e'_5.h.e'_5
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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ (∡ p₁ p₂ p₃).tan⁻¹ = (∡ p₃ p₁ s.center).tan

Tactic:
convert (Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi _).symm

Result:
case h.e'_2.h.e'_5.h.e'_5.h.e'_5.convert_3
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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ 2 • ∡ p₁ p₂ p₃ + 2 • ∡ p₃ p₁ s.center = ↑π

Proof state:
case h.e'_2.h.e'_5.h.e'_5.h.e'_5.convert_3
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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ 2 • ∡ p₁ p₂ p₃ + 2 • ∡ p₃ p₁ s.center = ↑π

Tactic:
rw [add_comm,
  two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_ennreal_eq_zero {x : ℝ≥0∞} : (x : EReal) = 0 ↔ x = 0

Proof state:
x : ℝ≥0∞
⊢ ↑x = 0 ↔ x = 0

Tactic:
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem triple_product_permutation (u v w : Fin 3 → R) : u ⬝ᵥ v ×₃ w = v ⬝ᵥ w ×₃ u

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 1 * w 2 - v 2 * w 1) + u 1 * (v 2 * w 0 - v 0 * w 2) + u 2 * (v 0 * w 1 - v 1 * w 0) =
    v 0 * (w 1 * u 2 - w 2 * u 1) + v 1 * (w 2 * u 0 - w 0 * u 2) + v 2 * (w 0 * u 1 - w 1 * u 0)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    v 0 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 0 +
        v 1 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 1 +
      v 2 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 2

Tactic:
norm_num

Result:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 1 * w 2 - v 2 * w 1) + u 1 * (v 2 * w 0 - v 0 * w 2) + u 2 * (v 0 * w 1 - v 1 * w 0) =
    v 0 * (w 1 * u 2 - w 2 * u 1) + v 1 * (w 2 * u 0 - w 0 * u 2) + v 2 * (w 0 * u 1 - w 1 * u 0)

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u

Tactic:
simp_rw [cross_apply, vec3_dotProduct]

Result:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    v 0 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 0 +
        v 1 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 1 +
      v 2 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 2
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_eq_iSup_finset' (s : ι' → α) :
    ⨆ i, s i = ⨆ t : Finset (PLift ι'), ⨆ i ∈ t, s (PLift.down i)

Proof state:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down

Tactic:
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]

Result:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ x, s (Equiv.plift x) = ⨆ i, s i.down

Proof state:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ x, s (Equiv.plift x) = ⨆ i, s i.down

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem ofLe_eq_comap_incl : ofLe h = K.comap K'.incl

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ ofLe h = comap K'.incl K

Tactic:
ext

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x✝ : ↥K'
⊢ x✝ ∈ ofLe h ↔ x✝ ∈ comap K'.incl K

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x✝ : ↥K'
⊢ x✝ ∈ ofLe h ↔ x✝ ∈ comap K'.incl K

Tactic:
rw [mem_ofLe]

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x✝ : ↥K'
⊢ ↑x✝ ∈ K ↔ x✝ ∈ comap K'.incl K

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x✝ : ↥K'
⊢ ↑x✝ ∈ K ↔ x✝ ∈ comap K'.incl K

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem Ref.cast_eq {aig1 aig2 : AIG α} (ref : Ref aig1)
    (h : aig1.decls.size ≤ aig2.decls.size) :
    (ref.cast h) = ⟨ref.gate, by have := ref.hgate; omega⟩ := rfl

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
this : ref.gate < aig1.decls.size
⊢ ref.gate < aig2.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
⊢ ref.gate < aig2.decls.size

Tactic:
have := ref.hgate

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
this : ref.gate < aig1.decls.size
⊢ ref.gate < aig2.decls.size
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
theorem map_apply_ιMulti (f : M →ₗ[R] N) (m : Fin n → M) :
    map n f (ιMulti R n m) = ιMulti R n (f ∘ m)

Proof state:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m : Fin n → M
⊢ (map n f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)

Tactic:
simp only [map, alternatingMapLinearEquiv_apply_ιMulti, AlternatingMap.compLinearMap_apply,
  Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
    x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega)

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
h : x.getLsbD (n + i) = true
this : n + i < w
⊢ i < w - n

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n < w
⊢ x >>> n = BitVec.cast ⋯ (0#n ++ extractLsb' n (w - n) x)

Tactic:
ext i hi

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ (x >>> n).getLsbD i = (BitVec.cast ⋯ (0#n ++ extractLsb' n (w - n) x)).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
h : x.getLsbD (n + i) = true
⊢ i < w - n

Tactic:
have := lt_of_getLsbD h

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
h : x.getLsbD (n + i) = true
this : n + i < w
⊢ i < w - n

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ (x >>> n).getLsbD i = (BitVec.cast ⋯ (0#n ++ extractLsb' n (w - n) x)).getLsbD i

Tactic:
simp only [getLsbD_ushiftRight, getLsbD_cast, getLsbD_append, getLsbD_extractLsb', getLsbD_zero,
  Bool.if_false_right, Bool.and_self_left, Bool.iff_and_self, decide_eq_true_eq]

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ x.getLsbD (n + i) = true → i < w - n

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n < w
⊢ n + (w - n) = w

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ x.getLsbD (n + i) = true → i < w - n

Tactic:
intros h

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
h : x.getLsbD (n + i) = true
⊢ i < w - n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem boole_getElem_le_countP (p : α → Bool) (l : Vector α n) (i : Nat) (h : i < n) :
    (if p l[i] then 1 else 0) ≤ l.countP p

Proof state:
α : Type u_1
n : Nat
p : α → Bool
l : Vector α n
i : Nat
h : i < n
⊢ (if p l[i] = true then 1 else 0) ≤ countP p l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
i : Nat
l : Array α
h : i < l.size
⊢ (if p { toArray := l, size_toArray := ⋯ }[i] = true then 1 else 0) ≤ countP p { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
p : α → Bool
i : Nat
l : Array α
h : i < l.size
⊢ (if p { toArray := l, size_toArray := ⋯ }[i] = true then 1 else 0) ≤ countP p { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.boole_getElem_le_countP]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_ne_nil_iff [LawfulBEq α] {xs : List α} {a : α} :
    xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
a : α
⊢ eraseP (fun x => a == x) xs ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
a : α
⊢ xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
a : α
⊢ eraseP (fun x => a == x) xs ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.left_eq_of_isDiameter (h₁₃ : s.IsDiameter p₁ p₃) (h₂₃ : s.IsDiameter p₂ p₃) :
    p₁ = p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ p₃ : P
h₁₃ : s.IsDiameter p₁ p₃
h₂₃ : s.IsDiameter p₂ p₃
⊢ p₁ = p₂

Tactic:
rw [← h₁₃.pointReflection_center_right, ← h₂₃.pointReflection_center_right]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_add_lem {x y z w : ℕ} (xy : Nonneg (⟨x, -y⟩ : ℤ√d)) (zw : Nonneg (⟨-z, w⟩ : ℤ√d)) :
    Nonneg (⟨x, -y⟩ + ⟨-z, w⟩ : ℤ√d)

Proof state:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
rw [add_def, neg_add_eq_sub]

Result:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg

Proof state:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg

Tactic:
rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this

Result:
no goals

Proof state:
d x y z w : ℕ
xy✝ : { re := ↑x, im := -↑y }.Nonneg
zw✝ : { re := -↑z, im := ↑w }.Nonneg
j k m n : ℕ
xy : SqLe (n + m + 1) d k 1
zw : SqLe (k + j + 1) 1 n d
t : 1 * (k + j + 1) * (k + j + 1) ≤ 1 * k * k := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
⊢ (k + j + 1) * (k + j + 1) ≤ k * k

Tactic:
simpa [one_mul] using t

Result:
no goals

Proof state:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
have : Nonneg ⟨Int.subNatNat x z, Int.subNatNat w y⟩ :=
  Int.subNatNat_elim x z
    (fun m n i => SqLe y d m 1 → SqLe n 1 w d → Nonneg ⟨i, Int.subNatNat w y⟩)
    (fun j k =>
      Int.subNatNat_elim w y
        (fun m n i => SqLe n d (k + j) 1 → SqLe k 1 m d → Nonneg ⟨Int.ofNat j, i⟩)
        (fun _ _ _ _ => trivial) fun m n xy zw => sqLe_cancel zw xy)
    (fun j k =>
      Int.subNatNat_elim w y
        (fun m n i => SqLe n d k 1 → SqLe (k + j + 1) 1 m d → Nonneg ⟨-[j+1], i⟩)
        (fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
        let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
        have : k + j + 1 ≤ k :=
          Nat.mul_self_le_mul_self_iff.1 (by simpa [one_mul] using t)
        absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
    (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)

Result:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem divOf_zero (x : k[G]) : x /ᵒᶠ 0 = x

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
x✝ : G
⊢ (x /ᵒᶠ 0) x✝ = x x✝

Tactic:
simp only [AddMonoidAlgebra.divOf_apply, zero_add]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
⊢ x /ᵒᶠ 0 = x

Tactic:
ext

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
x✝ : G
⊢ (x /ᵒᶠ 0) x✝ = x x✝
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem BaireMeasurableSet.residualEq_isOpen (h : BaireMeasurableSet s) :
    ∃ u : Set α, (IsOpen u) ∧ s =ᵇ u

Proof state:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Tactic:
rcases ht.residualEq_isOpen with ⟨u, hu, htu⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
u : Set α
hu : IsOpen u
htu : t =ᶠ[residual α] u
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Tactic:
borelize α

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
u : Set α
hu : IsOpen u
htu : t =ᶠ[residual α] u
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Tactic:
exact ⟨u, hu, hst.trans htu⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Tactic:
rcases h with ⟨t, ht, hst⟩

Result:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply_eq_top [MeasurableSingletonClass α] : count s = ∞ ↔ s.Infinite

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
change s.Infinite at hs

Result:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Infinite
⊢ count s = ⊤ ↔ s.Infinite

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
by_cases hs : s.Finite

Result:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Finite
⊢ count s = ⊤ ↔ s.Infinite

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ⊤ ↔ s.Infinite

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Infinite
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
simp [hs, count_apply_infinite]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Finite
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
exact count_apply_eq_top' hs.measurableSet

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_le_toIcoMod_add (a b : α) : toIocMod hp a b ≤ toIcoMod hp a b + p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b ≤ toIocDiv hp a b + 1

Tactic:
apply (toIocDiv_wcovBy_toIcoDiv _ _ _).le_succ

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b ≤ toIcoMod hp a b + p

Tactic:
rw [toIcoMod, toIocMod, sub_add, sub_le_sub_iff_left, sub_le_iff_le_add, ← add_one_zsmul,
  (zsmul_left_strictMono hp).le_iff_le]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b ≤ toIocDiv hp a b + 1
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_surjective_eq_arrow_of_lift_le (lle : lift.{u} #β' ≤ lift.{v} #α) :
    #{f : α → β' | Surjective f} = #(α → β') :=
  (mk_set_le _).antisymm <|
    have ⟨e⟩ : Nonempty (α ≃ α ⊕ β')

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α

Tactic:
exact add_eq_left (aleph0_le_lift.mpr <| aleph0_le_mk α) lle

Result:
no goals

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'

Tactic:
rw [lift_umax.{u,v}, eq_comm]

Result:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]

Result:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : α ≃ α ⊕ β'
f g : α → β'
h : (fun f => ⟨fun a => Sum.elim f id (e a), ⋯⟩) f = (fun f => ⟨fun a => Sum.elim f id (e a), ⋯⟩) g
a : α
⊢ f a = g a

Tactic:
simpa only [e.apply_symm_apply] using congr_fun (Subtype.ext_iff.mp h) (e.symm <| .inl a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
  | [], _ => by simp
  | a::l, 0 => by simp
  | a::l, k + 1 => by simp [eraseIdx_sublist l k]

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).eraseIdx 0 <+ a :: l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x✝ : Nat
⊢ [].eraseIdx x✝ <+ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
k : Nat
⊢ (a :: l).eraseIdx (k + 1) <+ a :: l

Tactic:
simp [eraseIdx_sublist l k]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_node4L (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
    dual (node4L l x m y r) = node4R (dual r) y (dual m) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual

Tactic:
cases m <;> simp [node4L, node4R, node3R, dual_node3L, dual_node', add_comm]

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_neg : ∀ n, ((-n : ℤ) : R) = -n
  | (0 : ℕ) => by simp
  | (n + 1 : ℕ) => by erw [cast_natCast, cast_negSucc]
  | -[n+1] => by erw [cast_natCast, cast_negSucc, neg_neg]

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(- -[n+1]) = -↑-[n+1]

Tactic:
erw [cast_natCast, cast_negSucc, neg_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)

Tactic:
erw [cast_natCast, cast_negSucc]

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
/-- If `f` is smooth of any relative dimension, it is smooth. -/
lemma IsSmoothOfRelativeDimension.isSmooth [IsSmoothOfRelativeDimension n f] : IsSmooth f where
  exists_isStandardSmooth x

Proof state:
case intro.intro.intro.intro
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSmoothOfRelativeDimension n f
x : ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
V : ↑X.affineOpens
hx : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).IsStandardSmooth

Tactic:
exact ⟨U, V, hx, e, hf.isStandardSmooth⟩

Result:
no goals

Proof state:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSmoothOfRelativeDimension n f
x : ↑↑X.toPresheafedSpace
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).IsStandardSmooth

Tactic:
obtain ⟨U, V, hx, e, hf⟩ := exists_isStandardSmoothOfRelativeDimension (n := n) (f := f) x

Result:
case intro.intro.intro.intro
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSmoothOfRelativeDimension n f
x : ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
V : ↑X.affineOpens
hx : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).IsStandardSmooth