harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/RCLike/Basic.lean
theorem normSq_sub (z w : K) : normSq (z - w) = normSq z + normSq w - 2 * re (z * conj w)

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ normSq (z - w) = normSq z + normSq w - 2 * re (z * (starRingEnd K) w)

Tactic:
simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem isLUB_sSup (h₁ : s.Nonempty) (h₂ : BddAbove s) : IsLUB s (sSup s)

Proof state:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (Classical.choose ⋯)

Tactic:
apply Classical.choose_spec

Result:
no goals

Proof state:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
simp only [sSup_def, dif_pos (And.intro h₁ h₂)]

Result:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (Classical.choose ⋯)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_sin_inj {θ ψ : ℝ} (Hcos : cos θ = cos ψ) (Hsin : sin θ = sin ψ) : (θ : Angle) = ψ

Proof state:
case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

Tactic:
exact hs

Result:
no goals

Proof state:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ

Tactic:
obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)

Result:
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ ↑θ = ↑ψ

Proof state:
case inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

Tactic:
exact hc

Result:
no goals

Proof state:
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ ↑θ = ↑ψ

Tactic:
rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
  eq_false (ne_of_gt pi_pos), or_false, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one,
  ← Int.cast_ofNat, ← Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn

Result:
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
⊢ ↑θ = ↑ψ

Proof state:
case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ

Tactic:
rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs

Result:
case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ

Proof state:
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : (n * 2 + 1) % 2 = 0 % 2
⊢ ↑θ = ↑ψ

Tactic:
rw [add_comm, Int.add_mul_emod_self] at this

Result:
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ

Proof state:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ

Tactic:
rw [eq_neg_iff_add_eq_zero, hs] at hc

Result:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ

Proof state:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ

Tactic:
rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc | hc

Result:
case inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ

Proof state:
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ

Tactic:
exact absurd this one_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).size =
      if m.contains k && (f (m.get? k)).isNone then
        m.size - 1
      else if !m.contains k && (f (m.get? k)).isSome then
        m.size + 1
      else
        m.size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).size =
    if (m.contains k && (f (m.get? k)).isNone) = true then m.size - 1
    else if (!m.contains k && (f (m.get? k)).isSome) = true then m.size + 1 else m.size

Tactic:
simp_to_raw using Raw₀.size_alter

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Real.lean
theorem equivalent_one_zero_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
    [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
    ∃ w : Fin (Module.finrank ℝ M) → ℝ,
      (∀ i, w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) :=
  let ⟨w, hw⟩ := Q.equivalent_signType_weighted_sum_squared
  ⟨(w ·), fun i ↦ by cases h : w i <;> simp [h], hw⟩

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (Module.finrank ℝ M) → SignType
hw : Equivalent Q (weightedSumSquares ℝ fun i => ↑(w i))
i : Fin (Module.finrank ℝ M)
⊢ (fun x => ↑(w x)) i = -1 ∨ (fun x => ↑(w x)) i = 0 ∨ (fun x => ↑(w x)) i = 1

Tactic:
cases h : w i <;> simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_iInter_eq_iInter_closure_of_iUnion_indep [hι : Nonempty ι] (Is : ι → Set α)
    (h : M.Indep (⋃ i, Is i)) : M.closure (⋂ i, Is i) = (⋂ i, M.closure (Is i))

Proof state:
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)

Tactic:
convert h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is)
  (by simp [subset_iUnion])

Result:
case h.e'_3
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ⋂ i, M.closure (Is i) = ⋂ J ∈ range Is, M.closure J

Proof state:
case h.e'_3
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ⋂ i, M.closure (Is i) = ⋂ J ∈ range Is, M.closure J

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ∀ J ∈ range Is, J ⊆ ⋃ i, Is i

Tactic:
simp [subset_iUnion]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem blunt_iff_not_pointed (S : ConvexCone 𝕜 E) : S.Blunt ↔ ¬S.Pointed

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
⊢ S.Blunt ↔ ¬S.Pointed

Tactic:
rw [pointed_iff_not_blunt, Classical.not_not]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem mul_primeFactors_disjUnion {a b : R} (ha : a ≠ 0) (hb : b ≠ 0)
    (hc : IsCoprime a b) :
    primeFactors (a * b) =
    (primeFactors a).disjUnion (primeFactors b) (disjoint_primeFactors hc)

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
hb : b ≠ 0
hc : IsCoprime a b
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b

Tactic:
simp_rw [primeFactors]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
hb : b ≠ 0
hc : IsCoprime a b
⊢ (normalizedFactors (a * b)).toFinset = (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
hb : b ≠ 0
hc : IsCoprime a b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
classical
rw [Finset.disjUnion_eq_union]
simp_rw [primeFactors]
rw [normalizedFactors_mul ha hb, Multiset.toFinset_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
hb : b ≠ 0
hc : IsCoprime a b
⊢ (normalizedFactors (a * b)).toFinset = (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset

Tactic:
rw [normalizedFactors_mul ha hb, Multiset.toFinset_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
hb : b ≠ 0
hc : IsCoprime a b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
rw [Finset.disjUnion_eq_union]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
hb : b ≠ 0
hc : IsCoprime a b
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b
-- Mathlib/Tactic/Module.lean
theorem sub_eq_eval₃ [Ring R] [AddCommGroup M] [Module R M] {a₁ : R × M} (a₂ : R × M)
    {l₁ l₂ l : NF R M} (h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval) :
    (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Tactic:
simp only [eval_cons, neg_smul, neg_add, sub_eq_add_neg, ← h, ← add_assoc]

Result:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) + -l₂.eval = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval + -l₂.eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) + -l₂.eval = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval + -l₂.eval

Tactic:
congr! 1

Result:
case h.e'_5
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval

Proof state:
case h.e'_5
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval

Tactic:
rw [add_comm, add_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_of_Z_eq_zero_left {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.addY P Q = (P x * Q z) ^ 3 * Q y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3)) -
        W'.a₁ * ((P x * Q z) ^ 2 * Q x) * (P x * Q z * Q z) -
      W'.a₃ * (P x * Q z * Q z) ^ 3 =
    (P x * Q z) ^ 3 * Q y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addY P Q = (P x * Q z) ^ 3 * Q y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_left hP hPz, negY, addX_of_Z_eq_zero_left hPz,
  addZ_of_Z_eq_zero_left hPz]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3)) -
        W'.a₁ * ((P x * Q z) ^ 2 * Q x) * (P x * Q z * Q z) -
      W'.a₃ * (P x * Q z * Q z) ^ 3 =
    (P x * Q z) ^ 3 * Q y
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iInf [Finite β] {f : β → L.BoundedFormula α n}
    {v : α → M} {v' : Fin n → M} :
    (iInf f).Realize v v' ↔ ∀ b, (f b).Realize v v'

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst✝ : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iInf f).Realize v v' ↔ ∀ (b : β), (f b).Realize v v'

Tactic:
simp only [iInf, realize_foldr_inf, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
  forall_exists_index, forall_apply_eq_imp_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/Angle.lean
lemma angle_one_left (hy : y ≠ 0) : angle 1 y = |y.arg|

Proof state:
y : ℂ
hy : y ≠ 0
⊢ angle 1 y = |y.arg|

Tactic:
simp [angle_eq_abs_arg, hy]

Result:
no goals
-- Mathlib/Data/Prod/TProd.lean
theorem elim_of_mem (hl : (i :: l).Nodup) (hj : j ∈ l) (v : TProd α (i :: l)) :
    v.elim (mem_cons_of_mem _ hj) = TProd.elim v.2 hj

Proof state:
case hji
ι : Type u
α : ι → Type v
j : ι
l : List ι
inst✝ : DecidableEq ι
hj : j ∈ l
hl : (j :: l).Nodup
v : TProd α (j :: l)
⊢ False

Tactic:
exact hl.not_mem hj

Result:
no goals

Proof state:
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst✝ : DecidableEq ι
hl : (i :: l).Nodup
hj : j ∈ l
v : TProd α (i :: l)
⊢ v.elim ⋯ = TProd.elim v.2 hj

Tactic:
apply elim_of_ne

Result:
case hji
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst✝ : DecidableEq ι
hl : (i :: l).Nodup
hj : j ∈ l
v : TProd α (i :: l)
⊢ j ≠ i

Proof state:
case hji
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst✝ : DecidableEq ι
hl : (i :: l).Nodup
hj : j ∈ l
v : TProd α (i :: l)
⊢ j ≠ i

Tactic:
rintro rfl

Result:
case hji
ι : Type u
α : ι → Type v
j : ι
l : List ι
inst✝ : DecidableEq ι
hj : j ∈ l
hl : (j :: l).Nodup
v : TProd α (j :: l)
⊢ False
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.add {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x + g x) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (fun x => f x + g x) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x => f x + g x) univ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x => f x + g x) univ x

Tactic:
exact hf.add hg

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
@[simp] lemma apply_evalEquiv_symm_apply (f : Dual R M) (g : Dual R (Dual R M)) :
    f ((evalEquiv R M).symm g) = g f

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = g f

Tactic:
rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
⊢ f ((evalEquiv R M).symm g) = g f

Tactic:
set m := (evalEquiv R M).symm g

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = g f
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_at_zero : p.smeval (0 : S) = (p.coeff 0) • (1 : S)

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ ((monomial (n + 1)) a).smeval 0 = ((monomial (n + 1)) a).coeff 0 • 1

Tactic:
rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
smul_zero]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁴ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
p q : R[X]
ph : p.smeval 0 = p.coeff 0 • 1
qh : q.smeval 0 = q.coeff 0 • 1
⊢ (p + q).smeval 0 = (p + q).coeff 0 • 1

Tactic:
simp_all only [smeval_add, coeff_add, add_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
⊢ p.smeval 0 = p.coeff 0 • 1

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp_all only [smeval_add, coeff_add, add_smul]
| h_monomial n a =>
  cases n with
  | zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
  | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
      smul_zero]

Result:
no goals

Proof state:
case h_monomial.zero
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
⊢ ((monomial 0) a).smeval 0 = ((monomial 0) a).coeff 0 • 1

Tactic:
simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n : ℕ
a : R
⊢ ((monomial n) a).smeval 0 = ((monomial n) a).coeff 0 • 1

Tactic:
cases n with
| zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
| succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
    smul_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/Rat.lean
lemma divInt_div_divInt_cancel_left {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
    n /. x / (d /. x) = n /. d

Proof state:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d

Tactic:
rw [div_eq_mul_inv, inv_divInt', divInt_mul_divInt_cancel hx]

Result:
no goals
-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
theorem abelian_radical_of_hasTrivialRadical [HasTrivialRadical R L] :
    IsLieAbelian (radical R L)

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ IsLieAbelian ↥(radical R L)

Tactic:
rw [HasTrivialRadical.radical_eq_bot]

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ IsLieAbelian ↥⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ IsLieAbelian ↥⊥

Tactic:
exact LieIdeal.isLieAbelian_of_trivial ..

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
/-- Two natural numbers are equal if and only if they have the same divisors. -/
lemma dvd_left_iff_eq : (∀ a : ℕ, a ∣ m ↔ a ∣ n) ↔ m = n :=
  ⟨fun h => Nat.dvd_antisymm ((h _).mp (Nat.dvd_refl _)) ((h _).mpr (Nat.dvd_refl _)),
    fun h n => by rw [h]⟩

Proof state:
m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ m ↔ n ∣ n✝

Tactic:
rw [h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_congr_fun {f g : α → ℝ≥0∞} {s : Set α} (hs : MeasurableSet s)
    (hfg : ∀ᵐ x ∂μ, x ∈ s → f x = g x) : ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ f =ᶠ[ae (μ.restrict s)] g

Tactic:
rw [EventuallyEq]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x = g x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x = g x

Tactic:
rwa [ae_restrict_iff' hs]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [lintegral_congr_ae]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ f =ᶠ[ae (μ.restrict s)] g
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem measure_univ : volume (Set.univ : Set (AddCircle T)) = ENNReal.ofReal T

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ ENNReal.ofReal T * (addHaarMeasure ⊤) ↑⊤ = ENNReal.ofReal T

Tactic:
simp [addHaarMeasure_self (G := AddCircle T), -PositiveCompacts.coe_top]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ ENNReal.ofReal T * (addHaarMeasure ⊤) univ = ENNReal.ofReal T

Tactic:
rw [← PositiveCompacts.coe_top]

Result:
T : ℝ
hT : Fact (0 < T)
⊢ ENNReal.ofReal T * (addHaarMeasure ⊤) ↑⊤ = ENNReal.ofReal T

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ volume univ = ENNReal.ofReal T

Tactic:
dsimp [volume]

Result:
T : ℝ
hT : Fact (0 < T)
⊢ ENNReal.ofReal T * (addHaarMeasure ⊤) univ = ENNReal.ofReal T
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma add_pow_expChar_of_commute (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p

Proof state:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime

Result:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + ↑p * r
⊢ (x + y) ^ p = x ^ p + y ^ p

Proof state:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + ↑p * r
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
simp [hr]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
obtain _ | hprime := hR

Result:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 = x ^ 1 + y ^ 1

case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Proof state:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 = x ^ 1 + y ^ 1

Tactic:
simp only [pow_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem sup_eq_range (p q : Submodule R M) : p ⊔ q = range (p.subtype.coprod q.subtype) :=
  Submodule.ext fun x => by simp [Submodule.mem_sup, SetLike.exists]

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
x : M
⊢ x ∈ p ⊔ q ↔ x ∈ range (p.subtype.coprod q.subtype)

Tactic:
simp [Submodule.mem_sup, SetLike.exists]

Result:
no goals