harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem tan_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
by_cases h0 : x = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
simp [h0]

Result:
no goals
-- Mathlib/Data/Fintype/Order.lean
theorem Directed.finite_le (D : Directed r f) (g : β → γ) : ∃ z, ∀ i, r (f (g i)) (f z)

Proof state:
case intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Finite β
D : Directed r f
g : β → γ
z : γ
hz : ∀ i ∈ Set.range g, r (f i) (f z)
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)

Tactic:
exact ⟨z, fun i => hz (g i) ⟨i, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Finite β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)

Tactic:
obtain ⟨z, hz⟩ := D.finite_set_le (Set.finite_range g)

Result:
case intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Finite β
D : Directed r f
g : β → γ
z : γ
hz : ∀ i ∈ Set.range g, r (f i) (f z)
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Finite β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)

Tactic:
classical
  obtain ⟨z, hz⟩ := D.finite_set_le (Set.finite_range g)
  exact ⟨z, fun i => hz (g i) ⟨i, rfl⟩⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[reassoc (attr := simp)]
lemma tensorCongr_trans_hom {x y z : Triplet f g} (e : x = y) (e' : y = z) :
    (tensorCongr e).hom ≫ (tensorCongr e').hom =
      (tensorCongr (e.trans e')).hom

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ (tensorCongr e).hom ≫ (tensorCongr e').hom = (tensorCongr ⋯).hom

Tactic:
subst e e'

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ (tensorCongr ⋯).hom ≫ (tensorCongr ⋯).hom = (tensorCongr ⋯).hom

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ (tensorCongr ⋯).hom ≫ (tensorCongr ⋯).hom = (tensorCongr ⋯).hom

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem isIntegrallyClosed_dvd_iff {s : S} (hs : IsIntegral R s) (p : R[X]) :
    Polynomial.aeval s p = 0 ↔ minpoly R s ∣ p :=
  ⟨fun hp => isIntegrallyClosed_dvd hs hp, fun hp => by
    simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom,
      Function.comp_apply, eval_map, ← aeval_def] using
      aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ (Polynomial.aeval s) p = 0

Tactic:
simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom,
  Function.comp_apply, eval_map, ← aeval_def] using
  aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem eq_one_of_sq_sub_mul_sq_eq_zero' {p : ℕ} [Fact p.Prime] {a : ℤ} (ha : (a : ZMod p) ≠ 0)
    {x y : ZMod p} (hx : x ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) : legendreSym p a = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hy : y ≠ 0
⊢ legendreSym p a = 1

Tactic:
exact eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * 0 ^ 2 = 0
⊢ False

Tactic:
rw [zero_pow two_ne_zero, mul_zero, sub_zero, sq_eq_zero_iff] at hxy

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ legendreSym p a = 1

Tactic:
haveI hy : y ≠ 0 := by
  rintro rfl
  rw [zero_pow two_ne_zero, mul_zero, sub_zero, sq_eq_zero_iff] at hxy
  exact hx hxy

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hy : y ≠ 0
⊢ legendreSym p a = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False

Tactic:
exact hx hxy

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * 0 ^ 2 = 0
⊢ False
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_right_Icc {a b c : α} (hab : a ≤ b) (hc : 0 ≤ c) :
    (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 < c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
exact image_mul_right_Icc' a b ‹0 < c›

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
hab : a ≤ b
hc : 0 ≤ c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
cases eq_or_lt_of_le hc

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 = c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 < c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b : α
hab : a ≤ b
hc : 0 ≤ 0
⊢ (fun x => x * 0) '' Icc a b = Icc (a * 0) (b * 0)

Tactic:
simp [(nonempty_Icc.2 hab).image_const]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 = c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
subst c

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b : α
hab : a ≤ b
hc : 0 ≤ 0
⊢ (fun x => x * 0) '' Icc a b = Icc (a * 0) (b * 0)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_finset [MeasurableSingletonClass α] (s : Finset α) (f : α → E)
    (hf : IntegrableOn f s μ) :
    ∫ x in s, f x ∂μ = ∑ x ∈ s, (μ {x}).toReal • f x

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Finset α
f : α → E
hf : IntegrableOn f (↑s) μ
⊢ ∫ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, (μ {x}).toReal • f x

Tactic:
rw [integral_countable _ s.countable_toSet hf, ← Finset.tsum_subtype']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem range_vecMulLinear (M : Matrix m n R) :
    LinearMap.range M.vecMulLinear = span R (range M)

Proof state:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R
      (Set.range fun x x_1 =>
        let j := x_1;
        Pi.single x 1 ⬝ᵥ fun i => M i j) =
    span R (Set.range M)

Tactic:
simp_rw [single_dotProduct, one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x => Pi.single x 1 ᵥ* M) = span R (Set.range M)

Tactic:
unfold vecMul

Result:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R
      (Set.range fun x x_1 =>
        let j := x_1;
        Pi.single x 1 ⬝ᵥ fun i => M i j) =
    span R (Set.range M)

Proof state:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ LinearMap.range M.vecMulLinear = span R (Set.range M)

Tactic:
letI := Classical.decEq m

Result:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ LinearMap.range M.vecMulLinear = span R (Set.range M)

Proof state:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ LinearMap.range M.vecMulLinear = span R (Set.range M)

Tactic:
simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ←
  Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
  Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, iUnion_singleton_eq_range,
  LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk]

Result:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x => Pi.single x 1 ᵥ* M) = span R (Set.range M)
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.add_right (hs : StarConvex 𝕜 x s) (z : E) :
    StarConvex 𝕜 (x + z) ((fun x => x + z) '' s)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ (fun x => x + z) (a • x + b • y') = a • (x + z) + b • (fun x => x + z) y'

Tactic:
match_scalars <;> simp [hab]

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (x + z) + b • (fun x => x + z) y' ∈ (fun x => x + z) '' s

Tactic:
refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ (fun x => x + z) (a • x + b • y') = a • (x + z) + b • (fun x => x + z) y'

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
⊢ StarConvex 𝕜 (x + z) ((fun x => x + z) '' s)

Tactic:
intro y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : y ∈ (fun x => x + z) '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x + z) + b • y ∈ (fun x => x + z) '' s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : y ∈ (fun x => x + z) '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x + z) + b • y ∈ (fun x => x + z) '' s

Tactic:
obtain ⟨y', hy', rfl⟩ := hy

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (x + z) + b • (fun x => x + z) y' ∈ (fun x => x + z) '' s
-- Mathlib/Algebra/Field/Periodic.lean
theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
    (hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc : c ≠ 0
a : α
⊢ f '' uIcc a (a + c) = range f

Tactic:
cases hc.lt_or_lt with
| inl hc =>
  rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
    add_neg_cancel_right]
| inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' uIcc a (a + c) = range f

Tactic:
rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
  add_neg_cancel_right]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' uIcc a (a + c) = range f

Tactic:
rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem eval₂_reflect_eq_zero_iff (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X])
    (hf : f.natDegree ≤ N) : eval₂ i (⅟ x) (reflect N f) = 0 ↔ eval₂ i x f = 0

Proof state:
case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) = 0

Tactic:
rw [← mul_one (eval₂ i (⅟ x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
  zero_mul]

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) = 0
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0

Tactic:
rw [h, zero_mul]

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) = 0

Proof state:
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i (⅟x) (reflect N f) * x ^ N = 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 → eval₂ i (⅟x) (reflect N f) * x ^ N = 0

case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0

Proof state:
case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 → eval₂ i (⅟x) (reflect N f) * x ^ N = 0

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) = 0
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0

Proof state:
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0

Tactic:
conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]

Result:
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i (⅟x) (reflect N f) * x ^ N = 0
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem sq_add_sq_ne_zero {R : Type*} [LinearOrderedCommRing R] {a b : R} (h : IsCoprime a b) :
    a ^ 2 + b ^ 2 ≠ 0

Proof state:
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
ha hb : 0 ^ 2 = 0
h : IsCoprime 0 0
h' : 0 ^ 2 + 0 ^ 2 = 0
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ False

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'

Result:
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
ha : a ^ 2 = 0
hb : b ^ 2 = 0
⊢ False

Proof state:
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
ha : a ^ 2 = 0
hb : b ^ 2 = 0
⊢ False

Tactic:
obtain rfl := pow_eq_zero ha

Result:
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
b : R
hb : b ^ 2 = 0
h : IsCoprime 0 b
h' : 0 ^ 2 + b ^ 2 = 0
ha : 0 ^ 2 = 0
⊢ False

Proof state:
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
b : R
hb : b ^ 2 = 0
h : IsCoprime 0 b
h' : 0 ^ 2 + b ^ 2 = 0
ha : 0 ^ 2 = 0
⊢ False

Tactic:
obtain rfl := pow_eq_zero hb

Result:
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
ha hb : 0 ^ 2 = 0
h : IsCoprime 0 0
h' : 0 ^ 2 + 0 ^ 2 = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
⊢ a ^ 2 + b ^ 2 ≠ 0

Tactic:
intro h'

Result:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ False
-- Mathlib/Probability/Moments/Basic.lean
lemma mgf_pos_iff [hμ : NeZero μ] :
    0 < mgf X μ t ↔ Integrable (fun ω ↦ exp (t * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t ≤ 0

Tactic:
simp [mgf_undef h]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : 0 < mgf X μ t
⊢ Integrable (fun ω => rexp (t * X ω)) μ

Tactic:
contrapose! h with h

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t ≤ 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
⊢ 0 < mgf X μ t ↔ Integrable (fun ω => rexp (t * X ω)) μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ mgf_pos' hμ.out h⟩

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : 0 < mgf X μ t
⊢ Integrable (fun ω => rexp (t * X ω)) μ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem rotateLeft_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
    BitVec.rotateLeft x' n = BitVec.rotateLeft x n

Proof state:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.rotateLeft n = x.rotateLeft n

Tactic:
simp[*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma X_ne_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P)
    (hPz : P z = 0) : P x ≠ 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P x ≠ 0

Tactic:
intro hPx

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x = 0
⊢ False

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x = 0
⊢ False

Tactic:
simp only [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPx, mul_zero, zero_mul,
  zero_pow <| OfNat.ofNat_ne_zero _, ne_self_iff_false, or_false, false_or] at hP

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : P y ^ 2 = 0 ∧ 2 * P y ≠ 0
⊢ False

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : P y ^ 2 = 0 ∧ 2 * P y ≠ 0
⊢ False

Tactic:
rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Reindex.lean
theorem reindexLinearEquiv_trans (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
    (reindexLinearEquiv R A e₁ e₂).trans (reindexLinearEquiv R A e₁' e₂') =
      (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : _ ≃ₗ[R] _)

Proof state:
case h.a
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
x✝ : Matrix m n A
i✝ : m''
j✝ : n''
⊢ (reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂') x✝ i✝ j✝ =
    (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) x✝ i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂' = reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')

Tactic:
ext

Result:
case h.a
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
x✝ : Matrix m n A
i✝ : m''
j✝ : n''
⊢ (reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂') x✝ i✝ j✝ =
    (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) x✝ i✝ j✝
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_C_mul_X_pow_le (n : ℕ) (a : R) : degree (C a * X ^ n) ≤ n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (C a * X ^ n).degree ≤ ↑n

Tactic:
rw [C_mul_X_pow_eq_monomial]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).degree ≤ ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).degree ≤ ↑n

Tactic:
apply degree_monomial_le

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem natDegree_primPart (p : R[X]) : p.primPart.natDegree = p.natDegree

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
conv_rhs =>
  rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.natDegree = p.natDegree

Tactic:
by_cases h : C p.content = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
rw [C_eq_zero, content_eq_zero_iff] at h

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.natDegree = p.natDegree