harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem eq_zero_or_opow_omega0_le_of_mul_eq_right {a b : Ordinal} (hab : a * b = b) :
    b = 0 ∨ a ^ ω ≤ b

Proof state:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b

Tactic:
exact Or.inr (Ordinal.zero_le b)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rcases eq_zero_or_pos a with ha | ha

Result:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b

Proof state:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b

Tactic:
intro hb

Result:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b

Proof state:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rw [ha, zero_opow omega0_ne_zero]

Result:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b

Proof state:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rw [or_iff_not_imp_left]

Result:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b

Proof state:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b

Tactic:
rw [← nfp_mul_one ha]

Result:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x => a * x) 1 ≤ b

Proof state:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x => a * x) 1 ≤ b

Tactic:
exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

Result:
no goals

Proof state:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x => a * x) 1 ≤ b

Tactic:
rw [← Ne, ← one_le_iff_ne_zero] at hb

Result:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x => a * x) 1 ≤ b
-- Mathlib/Analysis/Normed/Affine/Simplex.lean
lemma equilateral_iff_dist_01_eq_02_and_dist_01_eq_12 {t : Triangle R P} :
    t.Equilateral ↔ dist (t.points 0) (t.points 1) = dist (t.points 0) (t.points 2) ∧
      dist (t.points 0) (t.points 1) = dist (t.points 1) (t.points 2) :=
  equilateral_iff_dist_eq_and_dist_eq (by decide) (by decide) (by decide)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ 0 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ 0 ≠ 2

Tactic:
decide

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ 1 ≠ 2

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
theorem go_denote_entry (entry : Entrypoint β) {h} :
    ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, h⟩, assign⟧ = ⟦entry, assign⟧

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
expr : BoolExpr α
entry : Entrypoint β
h : entry.ref.gate < (go entry.aig expr atomHandler).val.aig.decls.size
⊢ ⟦assign, { aig := (go entry.aig expr atomHandler).val.aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ =
    ⟦assign, entry⟧

Tactic:
apply denote.eq_of_isPrefix

Result:
case hprefix
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
expr : BoolExpr α
entry : Entrypoint β
h : entry.ref.gate < (go entry.aig expr atomHandler).val.aig.decls.size
⊢ IsPrefix entry.aig.decls (go entry.aig expr atomHandler).val.aig.decls

Proof state:
case hprefix
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
expr : BoolExpr α
entry : Entrypoint β
h : entry.ref.gate < (go entry.aig expr atomHandler).val.aig.decls.size
⊢ IsPrefix entry.aig.decls (go entry.aig expr atomHandler).val.aig.decls

Tactic:
apply ofBoolExprCached.go_isPrefix_aig

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem of_mul_inv_t (a : A) :
    (of (a : G) : HNNExtension G A B φ) * t⁻¹ = t⁻¹ * of (φ a : G)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * (t * of ↑a * t⁻¹)

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * of ↑(φ a)

Tactic:
rw [equiv_eq_conj]

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * (t * of ↑a * t⁻¹)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem hasStrictDerivAt_cos (x : ℂ) : HasStrictDerivAt cos (-sin x) x

Proof state:
case h.e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ HasStrictDerivAt cos (-sin x) x

Tactic:
simp only [sin, div_eq_mul_inv, neg_mul_eq_neg_mul]

Result:
x : ℂ
⊢ HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x

Proof state:
case h.e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹

Tactic:
simp only [Function.comp, id]

Result:
case h.e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹

Proof state:
x : ℂ
⊢ HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x

Tactic:
convert (((hasStrictDerivAt_id x).mul_const I).cexp.add
  ((hasStrictDerivAt_id x).neg.mul_const I).cexp).mul_const (2 : ℂ)⁻¹ using 1

Result:
case h.e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem iUnion_pi_of_monotone {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type*}
    {I : Set ι} {s : ∀ i, ι' → Set (α i)} (hI : I.Finite) (hs : ∀ i ∈ I, Monotone (s i)) :
    ⋃ j : ι', I.pi (fun i => s i j) = I.pi fun i => ⋃ j, s i j

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite ↑I
i : ↑I
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval ↑i ⁻¹' s (↑i) j₁ ≤ eval ↑i ⁻¹' s (↑i) j₂

Tactic:
exact preimage_mono <| hs i i.2 h

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ (⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j

Tactic:
simp only [pi_def, biInter_eq_iInter, preimage_iUnion]

Result:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ ⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ ⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i

Tactic:
haveI := hI.fintype.finite

Result:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite ↑I
⊢ ⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite ↑I
⊢ ⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i

Tactic:
refine iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)

Result:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite ↑I
i : ↑I
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval ↑i ⁻¹' s (↑i) j₁ ≤ eval ↑i ⁻¹' s (↑i) j₂
-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem unique_irreducible [ValuationRing R] ⦃p q : R⦄ (hp : Irreducible p) (hq : Irreducible q) :
    Associated p q

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q

Tactic:
have := dvd_total p q

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : p ∣ q ∨ q ∣ p
⊢ Associated p q

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : p ∣ q ∨ q ∣ p
⊢ Associated p q

Tactic:
rw [Irreducible.dvd_comm hp hq, or_self_iff] at this

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q

Tactic:
exact associated_of_dvd_dvd (Irreducible.dvd_symm hq hp this) this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
    getD (m.insertIfNew k v) a fallback =
      if k == a ∧ ¬k ∈ m then v else getD m a fallback

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else getD m a fallback

Tactic:
exact Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ ¬k ∈ m then v else getD m a fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else getD m a fallback
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_eq_zero_iff_eq_C {p : MvPolynomial σ R} :
    p.totalDegree = 0 ↔ p = C (p.coeff 0)

Proof state:
case neg.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ p.totalDegree < ∑ i ∈ m.support, m i

Tactic:
rw [h]

Result:
case neg.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ 0 < ∑ i ∈ m.support, m i

Proof state:
case mp.a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0

Tactic:
split_ifs with hm

Result:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0

Proof state:
case neg.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ 0 < ∑ i ∈ m.support, m i

Tactic:
exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
  (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p = C (coeff 0 p)

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)

case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0

Proof state:
case mp.a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))

Tactic:
rw [coeff_C]

Result:
case mp.a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0

Proof state:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)

Tactic:
ext m

Result:
case mp.a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0

Tactic:
apply coeff_eq_zero_of_totalDegree_lt

Result:
case neg.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ p.totalDegree < ∑ i ∈ m.support, m i

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

Tactic:
rw [← hm]

Result:
no goals

Proof state:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0

Tactic:
rw [h, totalDegree_C]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.inner_map_self_eq_zero {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
    (∀ x, ⟪T x, x⟫ = 0) ↔ T = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), inner (T x) x = 0
x : E
⊢ (inner (T (x + T x)) (x + T x) - inner (T (x - T x)) (x - T x) - I * inner (T (x + I • T x)) (x + I • T x) +
        I * inner (T (x - I • T x)) (x - I • T x)) /
      4 =
    0

Tactic:
simp_rw [h _]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), inner (T x) x = 0
x : E
⊢ (0 - 0 - I * 0 + I * 0) / 4 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), T x = 0
⊢ ∀ (x : E), inner (T x) x = 0

Tactic:
simp_rw [h, inner_zero_left, forall_const]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), inner (T x) x = 0
x : E
⊢ (0 - 0 - I * 0 + I * 0) / 4 = 0

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ (∀ (x : E), inner (T x) x = 0) ↔ ∀ (x : E), T x = 0

Tactic:
refine ⟨fun h x => ?_, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), inner (T x) x = 0
x : E
⊢ T x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ (∀ (x : E), inner (T x) x = 0) ↔ T = 0

Tactic:
simp_rw [LinearMap.ext_iff, zero_apply]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ (∀ (x : E), inner (T x) x = 0) ↔ ∀ (x : E), T x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), inner (T x) x = 0
x : E
⊢ T x = 0

Tactic:
rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), inner (T x) x = 0
x : E
⊢ (inner (T (x + T x)) (x + T x) - inner (T (x - T x)) (x - T x) - I * inner (T (x + I • T x)) (x + I • T x) +
        I * inner (T (x - I • T x)) (x - I • T x)) /
      4 =
    0
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_piFinTwo {α : Fin 2 → Type u} {m : ∀ i, MeasurableSpace (α i)}
    (μ : ∀ i, Measure (α i)) [∀ i, SigmaFinite (μ i)] :
    MeasurePreserving (MeasurableEquiv.piFinTwo α) (Measure.pi μ) ((μ 0).prod (μ 1))

Proof state:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ) ((μ 0).prod (μ 1))

Tactic:
refine ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => ?_).symm⟩

Result:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (Measure.map (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = (μ 0) s * (μ 1) t

Proof state:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * (μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) = (μ 0) s * (μ 1) t

Tactic:
rfl

Result:
no goals

Proof state:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (Measure.map (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = (μ 0) s * (μ 1) t

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod,
  Measure.pi_pi, Fin.prod_univ_two]

Result:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * (μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) = (μ 0) s * (μ 1) t
-- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
theorem nonarchimedean : @NonarchimedeanRing A _ hB.topology

Proof state:
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U

Tactic:
obtain ⟨i, -, hi : (B i : Set A) ⊆ U⟩ := hB.hasBasis_nhds_zero.mem_iff.mp hU

Result:
case is_nonarchimedean.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U

Proof state:
case is_nonarchimedean.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U

Tactic:
exact ⟨hB.openAddSubgroup i, hi⟩

Result:
no goals

Proof state:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
⊢ NonarchimedeanRing A

Tactic:
constructor

Result:
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Proof state:
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U hU

Result:
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U

Proof state:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ NonarchimedeanRing A

Tactic:
letI := hB.topology

Result:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
⊢ NonarchimedeanRing A
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_C_mul : divX (C a * p) = C a * divX p

Proof state:
case a
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (C a * p).divX.coeff n✝ = (C a * p.divX).coeff n✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
⊢ (C a * p).divX = C a * p.divX

Tactic:
ext

Result:
case a
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (C a * p).divX.coeff n✝ = (C a * p.divX).coeff n✝
-- Mathlib/LinearAlgebra/SModEq.lean
theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ x₁ + x₂ ≡ y₁ + y₂ [SMOD U]

Tactic:
rw [SModEq.def] at hxy₁ hxy₂ ⊢

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk (x₁ + x₂) = Submodule.Quotient.mk (y₁ + y₂)

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk (x₁ + x₂) = Submodule.Quotient.mk (y₁ + y₂)

Tactic:
simp_rw [Quotient.mk_add, hxy₁, hxy₂]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem min_def_lt (x y : α) : min x y = if x < y then x else y

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ (if ¬y ≤ x then x else y) = if x < y then x else y

Tactic:
simp only [not_le]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ x ⊓ y = if x < y then x else y

Tactic:
rw [min_comm, min_def, ← ite_not]

Result:
α : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ (if ¬y ≤ x then x else y) = if x < y then x else y
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem opRingEquiv_single [Monoid G] (r : k) (x : G) :
    MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
r : k
x : G
⊢ MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Tactic:
simp

Result:
no goals