harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma isMaximalClique_compl (s : Finset α) :
    Maximal Gᶜ.IsClique s ↔ Maximal G.IsIndepSet s

Proof state:
α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsClique ↑s ↔ Maximal G.IsIndepSet ↑s

Tactic:
simp [isMaximalIndepSet_iff, isMaximalClique_iff]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem coprime_sq_sub_sq_add_of_odd_even {m n : ℤ} (h : Int.gcd m n = 1) (hm : m % 2 = 1)
    (hn : n % 2 = 0) : Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ n.gcd m = 1

Tactic:
rwa [Int.gcd_comm]

Result:
no goals

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2

Tactic:
ring

Result:
no goals

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (n ^ 2 + m ^ 2).natAbs = 1

Tactic:
apply coprime_sq_sub_sq_add_of_even_odd _ hn hm

Result:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ n.gcd m = 1

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (m ^ 2 + n ^ 2).natAbs = 1

Tactic:
rw [(by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2), add_comm]

Result:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (n ^ 2 + m ^ 2).natAbs = 1

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1

Tactic:
rw [Int.gcd, ← Int.natAbs_neg (m ^ 2 - n ^ 2)]

Result:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (m ^ 2 + n ^ 2).natAbs = 1
-- Mathlib/Order/SuccPred/Limit.lean
lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
    IsSuccPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
⊢ False

Tactic:
obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt

Result:
case intro.intro.intro
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
⊢ False

Tactic:
obtain rfl := (hb.ge_of_gt hbc).antisymm hca

Result:
case intro.intro.intro
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
hc : a ∈ s
hbc : b < a
hca : a ≤ a
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
hc : a ∈ s
hbc : b < a
hca : a ≤ a
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
⊢ IsSuccPrelimit a

Tactic:
intro b hb

Result:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
⊢ False
-- Mathlib/Data/List/Palindrome.lean
theorem of_reverse_eq {l : List α} : reverse l = l → Palindrome l

Proof state:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
this : l.Palindrome
⊢ (x :: (l ++ [x])).Palindrome

Tactic:
exact Palindrome.cons_concat x this

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.reverse = l → l.Palindrome

Tactic:
refine bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) ?_

Result:
α : Type u_1
l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome

Proof state:
α : Type u_1
l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome

Tactic:
intro x l y hp hr

Result:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Proof state:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Tactic:
rw [head_eq_of_cons_eq hr]

Result:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [x])).Palindrome

Proof state:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Tactic:
rw [reverse_cons, reverse_append] at hr

Result:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Proof state:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [x])).Palindrome

Tactic:
have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)

Result:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
this : l.Palindrome
⊢ (x :: (l ++ [x])).Palindrome
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableWithinAt.comp_of_eq {y : M'} (hg : MDifferentiableWithinAt I' I'' g u y)
    (hf : MDifferentiableWithinAt I I' f s x) (h : s ⊆ f ⁻¹' u) (hy : f x = y) :
    MDifferentiableWithinAt I I'' (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact hg.comp _ hf h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
y : M'
hg : MDifferentiableWithinAt I' I'' g u y
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hy : f x = y
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃)
    (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

Proof state:
case a
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) = f x

Tactic:
simp only [hf _]

Result:
no goals

Proof state:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ g.ker

Tactic:
apply hg

Result:
case a
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ f.ker

Proof state:
case a
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]

Result:
case a
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) = f x

Proof state:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

Tactic:
dsimp [liftOfRightInverseAux]

Result:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) = g x

Proof state:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) = g x

Tactic:
rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]

Result:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ g.ker
-- Mathlib/Data/Part.lean
theorem mul_mem_mul [Mul α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma * mb ∈ a * b := ⟨⟨ha.1, hb.1⟩, by simp only [← ha.2, ← hb.2]; rfl⟩

Proof state:
α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = a.get ⋯ * b.get ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = ma * mb

Tactic:
simp only [← ha.2, ← hb.2]

Result:
α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = a.get ⋯ * b.get ⋯
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem continuous_infEdist : Continuous fun x => infEdist x s :=
  continuous_of_le_add_edist 1 (by simp) <| by
    simp only [one_mul, infEdist_le_infEdist_add_edist, forall₂_true_iff]

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ 1 ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ (x y : α), infEdist x s ≤ infEdist y s + 1 * edist x y

Tactic:
simp only [one_mul, infEdist_le_infEdist_add_edist, forall₂_true_iff]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma conjugate_le_norm_smul' {a b : A} (hb : IsSelfAdjoint b

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
h₂ : a * star a = star (star a) * star a
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Tactic:
simp only [h₁, h₂]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
h₂ : a * star a = star (star a) * star a
⊢ star (star a) * b * star a ≤ ‖b‖ • (star (star a) * star a)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Tactic:
have h₁ : a * b * star a = star (star a) * b * star a := by simp

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
h₂ : a * star a = star (star a) * star a
⊢ star (star a) * b * star a ≤ ‖b‖ • (star (star a) * star a)

Tactic:
exact conjugate_le_norm_smul

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
⊢ a * star a = star (star a) * star a

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Tactic:
have h₂ : a * star a = star (star a) * star a := by simp

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
h₁ : a * b * star a = star (star a) * b * star a
h₂ : a * star a = star (star a) * star a
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ a * b * star a = star (star a) * b * star a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_neg_coe_angle {x : ℂ} (hx : x ≠ 0) : (arg (-x) : Real.Angle) = arg x + π

Proof state:
case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
exact False.elim (hx (ext hr hi))

Result:
no goals

Proof state:
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
rw [(ext rfl hi : x = x.re)]

Result:
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Proof state:
x : ℂ
hx : x ≠ 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
rcases lt_trichotomy x.im 0 with (hi | hi | hi)

Result:
case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π

Proof state:
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le, ←
  Real.Angle.coe_add, ← two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]

Result:
no goals

Proof state:
case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]

Result:
no goals

Proof state:
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Result:
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Proof state:
case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr),
  Real.Angle.coe_zero, zero_add]

Result:
no goals

Proof state:
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
rw [arg_neg_eq_arg_sub_pi_of_im_pos hi, Real.Angle.coe_sub, Real.Angle.sub_coe_pi_eq_add_coe_pi]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma fderiv_fourierChar_neg_bilinear_right_apply (v : V) (w y : W) :
    fderiv ℝ (fun w ↦ (𝐞 (-L v w) : ℂ)) w y = -2 * π * I * L v y * 𝐞 (-L v w)

Proof state:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w y : W
⊢ (fderiv ℝ (fun w => ↑(𝐞 (-(L v) w))) w) y = -2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))

Tactic:
simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul,
  ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
  Function.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]

Result:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = 2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))

Proof state:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = 2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem?_enumFrom :
    ∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a)
  | _, [], _ => rfl
  | _, _ :: _, 0 => by simp
  | n, _ :: l, m + 1 => by
    simp only [enumFrom_cons, getElem?_cons_succ]
    exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl

Proof state:
α : Type u_1
n : Nat
head✝ : α
l : List α
m : Nat
⊢ (enumFrom (n + 1) l)[m]? = Option.map (fun a => (n + (m + 1), a)) l[m]?

Tactic:
exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
head✝ : α
l : List α
m : Nat
⊢ Option.map (fun a => (n + 1 + m, a)) l[m]? = Option.map (fun a => (n + (m + 1), a)) l[m]?

Tactic:
rw [Nat.add_right_comm]

Result:
α : Type u_1
n : Nat
head✝ : α
l : List α
m : Nat
⊢ Option.map (fun a => (n + m + 1, a)) l[m]? = Option.map (fun a => (n + (m + 1), a)) l[m]?

Proof state:
α : Type u_1
x✝ : Nat
head✝ : α
tail✝ : List α
⊢ (enumFrom x✝ (head✝ :: tail✝))[0]? = Option.map (fun a => (x✝ + 0, a)) (head✝ :: tail✝)[0]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
head✝ : α
l : List α
m : Nat
⊢ Option.map (fun a => (n + m + 1, a)) l[m]? = Option.map (fun a => (n + (m + 1), a)) l[m]?

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
head✝ : α
l : List α
m : Nat
⊢ (enumFrom n (head✝ :: l))[m + 1]? = Option.map (fun a => (n + (m + 1), a)) (head✝ :: l)[m + 1]?

Tactic:
simp only [enumFrom_cons, getElem?_cons_succ]

Result:
α : Type u_1
n : Nat
head✝ : α
l : List α
m : Nat
⊢ (enumFrom (n + 1) l)[m]? = Option.map (fun a => (n + (m + 1), a)) l[m]?
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@[to_additive]
lemma mul_le_of_forall_lt [CommGroup α] [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
    [DenselyOrdered α] {a b c : α} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) :
    a * b ≤ c

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd✝ : d < a * b
a' : α
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd✝¹ : d < a * b
a' : α
ha' : a' < a
hd✝ : d < a' * b
b' : α
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd✝¹ : d < a * b
a' : α
ha' : a' < a
hd✝ : d < a' * b
b' : α
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Tactic:
exact hd.le.trans (h a' ha' b' hb')

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd : d < a * b
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd

Result:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd✝ : d < a * b
a' : α
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c

Proof state:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Result:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 ≤ x2
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd : d < a * b
⊢ d ≤ c
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma fromAffine_ne_zero [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) :
    fromAffine (.some h) ≠ 0 := fun h0 ↦ by
  obtain ⟨u, eq⟩ := Quotient.eq.mp <| (Point.ext_iff ..).mp h0
  simpa [Units.smul_def, smul_fin3] using congr_fun eq z

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
X Y : R
h : (toAffine W').Nonsingular X Y
h0 : fromAffine (Affine.Point.some h) = 0
⊢ False

Tactic:
obtain ⟨u, eq⟩ := Quotient.eq.mp <| (Point.ext_iff ..).mp h0

Result:
case intro
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
X Y : R
h : (toAffine W').Nonsingular X Y
h0 : fromAffine (Affine.Point.some h) = 0
u : Rˣ
eq : (fun m => m • ![0, 1, 0]) u = ![X, Y, 1]
⊢ False

Proof state:
case intro
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
X Y : R
h : (toAffine W').Nonsingular X Y
h0 : fromAffine (Affine.Point.some h) = 0
u : Rˣ
eq : (fun m => m • ![0, 1, 0]) u = ![X, Y, 1]
⊢ False

Tactic:
simpa [Units.smul_def, smul_fin3] using congr_fun eq z

Result:
no goals