harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sign.lean
theorem Right.sign_neg [AddRightStrictMono α] (a : α) :
    sign (-a) = -sign a

Proof state:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]

Result:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Proof state:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

Tactic:
exact False.elim (lt_asymm h h')

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Tactic:
split_ifs with h h'

Result:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Proof state:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem ysq_dvd_yy (n) : yn a1 n * yn a1 n ∣ yn a1 (n * yn a1 n) :=
  modEq_zero_iff_dvd.1 <|
    ((xy_modEq_yn a1 n (yn a1 n)).right.of_dvd <| by simp [_root_.pow_succ]).trans
      (modEq_zero_iff_dvd.2 <| by simp [mul_dvd_mul_left, mul_assoc])

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 n * yn a1 n ∣ yn a1 n ^ 3

Tactic:
simp [_root_.pow_succ]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 n * yn a1 n ∣ yn a1 n * xn a1 n ^ (yn a1 n - 1) * yn a1 n

Tactic:
simp [mul_dvd_mul_left, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem one_or_eq_of_le_of_prime {p m : Associates M} (hp : Prime p) (hle : m ≤ p) :
    m = 1 ∨ m = p

Proof state:
case intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime (Associates.mk p)
m : M
hle : Associates.mk m ≤ Associates.mk p
⊢ Associates.mk m = 1 ∨ Associates.mk m = Associates.mk p

Tactic:
simpa [mk_eq_mk_iff_associated, Associated.comm, -Quotient.eq]
  using (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
m : Associates M
p : M
hp : Prime (Associates.mk p)
hle : m ≤ Associates.mk p
⊢ m = 1 ∨ m = Associates.mk p

Tactic:
rcases mk_surjective m with ⟨m, rfl⟩

Result:
case intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime (Associates.mk p)
m : M
hle : Associates.mk m ≤ Associates.mk p
⊢ Associates.mk m = 1 ∨ Associates.mk m = Associates.mk p

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p m : Associates M
hp : Prime p
hle : m ≤ p
⊢ m = 1 ∨ m = p

Tactic:
rcases mk_surjective p with ⟨p, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
m : Associates M
p : M
hp : Prime (Associates.mk p)
hle : m ≤ Associates.mk p
⊢ m = 1 ∨ m = Associates.mk p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_lt_two_pow_iff : 1 < 2 ^ n ↔ n ≠ 0 :=
  ⟨(by intro h p; subst p; simp at h), Nat.one_lt_two_pow⟩

Proof state:
n : Nat
⊢ 1 < 2 ^ n → n ≠ 0

Tactic:
intro h p

Result:
n : Nat
h : 1 < 2 ^ n
p : n = 0
⊢ False

Proof state:
h : 1 < 2 ^ 0
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
n : Nat
h : 1 < 2 ^ n
p : n = 0
⊢ False

Tactic:
subst p

Result:
h : 1 < 2 ^ 0
⊢ False
-- Mathlib/Topology/Sets/Closeds.lean
lemma Closeds.coe_eq_singleton_of_isAtom [T0Space α] {s : Closeds α} (hs : IsAtom s) :
    ∃ a, (s : Set α) = {a}

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
⊢ ∃ a, ↑s = {a}

Tactic:
refine minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_

Result:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
t : Set α
hts : t ⊆ ↑s
ht : t.Nonempty
ht' : IsClosed t
⊢ t = ↑s

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
t : Set α
hts : t ⊆ ↑s
ht : t.Nonempty
ht' : IsClosed t
⊢ t = ↑s

Tactic:
lift t to Closeds α using ht'

Result:
case intro
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
t : Closeds α
hts : ↑t ⊆ ↑s
ht : (↑t).Nonempty
⊢ ↑t = ↑s

Proof state:
case intro
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
t : Closeds α
hts : ↑t ⊆ ↑s
ht : (↑t).Nonempty
⊢ ↑t = ↑s

Tactic:
exact SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem null_of_frequently_le_of_frequently_ge {c d : ℝ≥0} (hcd : c < d) (s : Set α)
    (hc : ∀ x ∈ s, ∃ᶠ a in v.filterAt x, ρ a ≤ c * μ a)
    (hd : ∀ x ∈ s, ∃ᶠ a in v.filterAt x, (d : ℝ≥0∞) * μ a ≤ ρ a) : μ s = 0

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
⊢ ∃ u ∈ 𝓝[s] x, μ u = 0

Tactic:
refine ⟨s ∩ o, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), ?_⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
⊢ μ (s ∩ o) = 0

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
⊢ μ (s ∩ o) = 0

Tactic:
let s' := s ∩ o

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s' : Set α := s ∩ o
⊢ μ (s ∩ o) = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem reverse_size (t : RBNode α) : t.reverse.size = t.size

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.size = t.size

Tactic:
simp [size_eq]

Result:
no goals
-- Mathlib/Order/Filter/FilterProduct.lean
theorem lt_def [Preorder β] : ((· < ·) : β* → β* → Prop) = LiftRel (· < ·)

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
⊢ (fun x1 x2 => x1 < x2) = LiftRel fun x1 x2 => x1 < x2

Tactic:
ext ⟨f⟩ ⟨g⟩

Result:
case h.mk.h.mk.a
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
x✝¹ : (↑φ).Germ β
f : α → β
x✝ : (↑φ).Germ β
g : α → β
⊢ Quot.mk (⇑((↑φ).germSetoid β)) f < Quot.mk (⇑((↑φ).germSetoid β)) g ↔
    LiftRel (fun x1 x2 => x1 < x2) (Quot.mk (⇑((↑φ).germSetoid β)) f) (Quot.mk (⇑((↑φ).germSetoid β)) g)

Proof state:
case h.mk.h.mk.a
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
x✝¹ : (↑φ).Germ β
f : α → β
x✝ : (↑φ).Germ β
g : α → β
⊢ Quot.mk (⇑((↑φ).germSetoid β)) f < Quot.mk (⇑((↑φ).germSetoid β)) g ↔
    LiftRel (fun x1 x2 => x1 < x2) (Quot.mk (⇑((↑φ).germSetoid β)) f) (Quot.mk (⇑((↑φ).germSetoid β)) g)

Tactic:
exact coe_lt

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp] lemma chainBot_zero : chainBot 0 β = β

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
β : Weight R L M
x✝ : L
⊢ (chainBot 0 β) x✝ = β x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
β : Weight R L M
⊢ chainBot 0 β = β

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
β : Weight R L M
x✝ : L
⊢ (chainBot 0 β) x✝ = β x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_congr {c : Clause α} {r1 r2 : α → β} (hw : ∀ v, Mem v c → r1 v = r2 v) :
    relabel r1 c = relabel r2 c

Proof state:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
v : α
p : Bool
h : (v, p) ∈ c
⊢ (r1 (v, p).fst, (v, p).snd) = (r2 (v, p).fst, (v, p).snd)

Tactic:
congr

Result:
case e_fst
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
v : α
p : Bool
h : (v, p) ∈ c
⊢ r1 (v, p).fst = r2 (v, p).fst

Proof state:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
⊢ List.map (fun x => (r1 x.fst, x.snd)) c = List.map (fun x => (r2 x.fst, x.snd)) c

Tactic:
rw [List.map_congr_left]

Result:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
⊢ ∀ (a : Literal α), a ∈ c → (r1 a.fst, a.snd) = (r2 a.fst, a.snd)

Proof state:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
⊢ relabel r1 c = relabel r2 c

Tactic:
simp only [relabel]

Result:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
⊢ List.map (fun x => (r1 x.fst, x.snd)) c = List.map (fun x => (r2 x.fst, x.snd)) c

Proof state:
case e_fst
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
v : α
p : Bool
h : (v, p) ∈ c
⊢ r1 (v, p).fst = r2 (v, p).fst

Tactic:
apply hw _ (mem_of h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
⊢ ∀ (a : Literal α), a ∈ c → (r1 a.fst, a.snd) = (r2 a.fst, a.snd)

Tactic:
intro ⟨v, p⟩ h

Result:
α : Type u_1
β : Type u_2
c : Clause α
r1 r2 : α → β
hw : ∀ (v : α), Mem v c → r1 v = r2 v
v : α
p : Bool
h : (v, p) ∈ c
⊢ (r1 (v, p).fst, (v, p).snd) = (r2 (v, p).fst, (v, p).snd)
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_inv_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Tactic:
rw [braiding_tensorUnit_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).hom ≫ (ρ_ X).inv) ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv

Tactic:
rw [Iso.inv_ext]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).hom ≫ (ρ_ X).inv) ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Tactic:
monoidal

Result:
no goals
-- Mathlib/LinearAlgebra/Reflection.lean
/-- A formula for $r_2 (r_1 r_2)^m x$, where $m$ is an integer. -/
lemma reflection_mul_reflection_mul_reflection_zpow_apply_self (m : ℤ)
    (t : R := f y * g x - 2) (ht : t = f y * g x - 2

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ (reflection hg * (reflection hf * reflection hg) ^ m) x =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R m) * -g x) • y

Tactic:
rw [LinearEquiv.mul_apply, reflection_mul_reflection_zpow_apply_self hf hg m t ht]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ (reflection hg)
      ((Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
        (Polynomial.eval t (S R (m - 1)) * -g x) • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R m) * -g x) • y

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ (reflection hg)
      ((Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
        (Polynomial.eval t (S R (m - 1)) * -g x) • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R m) * -g x) • y

Tactic:
simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • (x - g x • y) +
      (Polynomial.eval t (S R (m - 1)) * -g x) • (y - 2 • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R m) * -g x) • y

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • (x - g x • y) +
      (Polynomial.eval t (S R (m - 1)) * -g x) • (y - 2 • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R m) * -g x) • y

Tactic:
module

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem coe_le_one (p : PMF α) (a : α) : p a ≤ 1

Proof state:
α : Type u_1
p : PMF α
a : α
⊢ p a ≤ 1

Tactic:
refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)

Result:
α : Type u_1
p : PMF α
a b : α
⊢ (if b = a then p a else 0) ≤ p b

Proof state:
α : Type u_1
p : PMF α
a b : α
⊢ (if b = a then p a else 0) ≤ p b

Tactic:
split_ifs with h <;> simp only [h, zero_le', le_rfl]

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
a : α
⊢ p a ≤ 1

Tactic:
classical
refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
split_ifs with h <;> simp only [h, zero_le', le_rfl]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_one_right (b : Ordinal) : log b 1 = 0

Proof state:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

Tactic:
exact log_eq_zero hb

Result:
no goals

Proof state:
b : Ordinal.{u_1}
⊢ log b 1 = 0

Tactic:
obtain hb | hb := lt_or_le 1 b

Result:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Proof state:
case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Tactic:
exact log_of_left_le_one hb 1

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
theorem ι_mul_ι_mul_invOf_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] :
    ι Q a * ι Q b * ⅟ (ι Q a) = ι Q ((⅟ (Q a) * QuadraticMap.polar Q a b) • a - b)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
a b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) a * (ι Q) b * ⅟((ι Q) a) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

Tactic:
rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
  invOf_mul_self, one_smul]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_top_iff_right (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOn N f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn N (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1))
            (fun x => (p x).shift) s

Proof state:
case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h :
  (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
      HasFTaylorSeriesUpToOn N (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
⊢ HasFTaylorSeriesUpToOn N f p s

Tactic:
apply (hasFTaylorSeriesUpToOn_top_iff_add hN 1).2 (fun n ↦ ?_)

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h :
  (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
      HasFTaylorSeriesUpToOn N (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isInt_zpow_pos {α : Type*} [DivisionRing α] {a : α} {b : ℤ} {nb ne : ℕ}
    (pb : IsNat b nb) (pe' : IsInt (a ^ nb) (Int.negOfNat ne)) :
    IsInt (a ^ b) (Int.negOfNat ne)

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, zpow_natCast]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Power.lean
theorem mul_norm_eq_abs_sub_sq_norm {x y z : V} (h₁ : ∃ k : ℝ, k ≠ 1 ∧ x + y = k • (x - y))
    (h₂ : ‖z - y‖ = ‖z + y‖) : ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₁ : ∃ k, k ≠ 1 ∧ x + y = k • (x - y)
h₂ : ‖z - y‖ = ‖z + y‖
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Tactic:
obtain ⟨k, hk_ne_one, hk⟩ := h₁

Result:
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Proof state:
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Tactic:
have hxy : x = r • y := by
  rw [← smul_smul, eq_inv_smul_iff₀ (sub_ne_zero.mpr hk_ne_one), ← sub_eq_zero]
  calc
    (k - 1) • x - (k + 1) • y = k • x - x - (k • y + y) := by
      simp_rw [sub_smul, add_smul, one_smul]
    _ = k • x - k • y - (x + y) := by simp_rw [← sub_sub, sub_right_comm]
    _ = k • (x - y) - (x + y) := by rw [← smul_sub k x y]
    _ = 0 := sub_eq_zero.mpr hk.symm

Result:
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2

Tactic:
ring

Result:
no goals