harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma comp_compProd_comm {η : Kernel (α × β) γ} [SFinite μ] [IsSFiniteKernel η] :
    η ∘ₘ (μ ⊗ₘ κ) = ((κ ⊗ₖ η) ∘ₘ μ).snd

Proof state:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ (⇑η ∘ₘ μ ⊗ₘ κ) s = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd s

Tactic:
rw [Measure.bind_apply hs η.measurable, Measure.snd_apply hs,
  Measure.bind_apply _ (Kernel.measurable _), Measure.lintegral_compProd (η.measurable_coe hs)]

Result:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (b : β), (η (a, b)) s ∂κ a ∂μ = ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.snd ⁻¹' s) ∂μ

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma inner_toCLM_conjTranspose_right {M : CStarMatrix m n A} {v : C⋆ᵐᵒᵈ (n → A)}
    {w : C⋆ᵐᵒᵈ (m → A)} : ⟪v, toCLM Mᴴ w⟫_A = ⟪toCLM M v, w⟫_A

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
w : C⋆ᵐᵒᵈ (m → A)
⊢ ⟪(toCLM M) v, w⟫_A = ⟪v, (toCLM Mᴴ) w⟫_A

Tactic:
simpa using inner_toCLM_conjTranspose_left (M := Mᴴ) (v := v) (w := w)

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
w : C⋆ᵐᵒᵈ (m → A)
⊢ ⟪v, (toCLM Mᴴ) w⟫_A = ⟪(toCLM M) v, w⟫_A

Tactic:
apply Eq.symm

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
w : C⋆ᵐᵒᵈ (m → A)
⊢ ⟪(toCLM M) v, w⟫_A = ⟪v, (toCLM Mᴴ) w⟫_A
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_X_add_pow (n k : ℕ) (c : R) :
    derivative^[k] ((X + C c) ^ n) = Nat.descFactorial n k • (X + C c) ^ (n - k)

Proof state:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
c : R
⊢ (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)

Tactic:
induction k with
| zero => simp
| succ k IH =>
    rw [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_smul,
      derivative_X_add_C_pow, map_natCast, Nat.descFactorial_succ, nsmul_eq_mul, nsmul_eq_mul,
      Nat.cast_mul]
    ring

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
⊢ (⇑derivative)^[0] ((X + C c) ^ n) = n.descFactorial 0 • (X + C c) ^ (n - 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * (X + C c) ^ (n - k - 1)) =
    ↑(n - k) * ↑(n.descFactorial k) * (X + C c) ^ (n - k - 1)

Tactic:
ring

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)
⊢ (⇑derivative)^[k + 1] ((X + C c) ^ n) = n.descFactorial (k + 1) • (X + C c) ^ (n - (k + 1))

Tactic:
rw [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_smul,
  derivative_X_add_C_pow, map_natCast, Nat.descFactorial_succ, nsmul_eq_mul, nsmul_eq_mul,
  Nat.cast_mul]

Result:
case succ
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * (X + C c) ^ (n - k - 1)) =
    ↑(n - k) * ↑(n.descFactorial k) * (X + C c) ^ (n - k - 1)
-- Mathlib/Analysis/Complex/Positivity.lean
theorem apply_le_of_iteratedDeriv_alternating {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f)
    (h : ∀ n ≠ 0, 0 ≤ (-1) ^ n * iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : z ≤ c) :
    f c ≤ f z

Proof state:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c ≤ f z

Tactic:
convert apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z))
  (hf.comp <| differentiable_neg) (fun n hn ↦ ?_) (neg_le_neg_iff.mpr hz) using 1

Result:
case h.e'_3
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c = f (- -c)

case h.e'_4
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f z = f (- -z)

f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n (fun z => f (-z)) (-c)

Proof state:
case h.e'_4
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f z = f (- -z)

Tactic:
simp only [neg_neg]

Result:
no goals

Proof state:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n (fun z => f (-z)) (-c)

Tactic:
simpa only [iteratedDeriv_comp_neg, neg_neg, smul_eq_mul] using h n hn

Result:
no goals

Proof state:
case h.e'_3
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c = f (- -c)

Tactic:
simp only [neg_neg]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable at `y ∈ S`, then the slope of any
secant line with right endpoint at `y` is strictly less than the left derivative at `y`. -/
lemma slope_lt_of_hasDerivWithinAt_Iio (hfc : StrictConvexOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Iio y) y)  :
    slope f x y < f'

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ slope f x y < f'

Tactic:
have := hfc.secant_strict_mono hy hx hu hxy.ne huy.ne hxu

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f x - f y) / (x - y) < (f u - f y) / (u - y)
⊢ slope f x y < f'

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f x - f y) / (x - y) < (f u - f y) / (u - y)
⊢ slope f x y < f'

Tactic:
simp_rw [← slope_def_field, slope_comm _ y] at this

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x y < slope f u y
⊢ slope f x y < f'

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x y < slope f u y
⊢ slope f x y < f'

Tactic:
exact this.trans_le <| hfc.convexOn.slope_le_of_hasDerivWithinAt_Iio hu hy huy hf'

Result:
no goals

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
⊢ slope f x y < f'

Tactic:
have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ slope f x y < f'

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y < f'

Tactic:
obtain ⟨u, hxu, huy⟩ := exists_between hxy

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
⊢ slope f x y < f'
-- Mathlib/Data/Real/EReal.lean
lemma antitone_div_right_of_nonpos (h : b ≤ 0) : Antitone fun a ↦ a / b

Proof state:
case h
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0

Tactic:
simp [h]

Result:
no goals

Proof state:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ 0 ≤ -b

Tactic:
apply EReal.le_neg_of_le_neg

Result:
case h
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0

Proof state:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ (fun a => a / b) a' ≤ (fun a => a / b) a

Tactic:
change a' * b⁻¹ ≤ a * b⁻¹

Result:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a' * b⁻¹ ≤ a * b⁻¹

Proof state:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Tactic:
have : 0 ≤ -b := by apply EReal.le_neg_of_le_neg; simp [h]

Result:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
this : 0 ≤ -b
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Proof state:
b : EReal
h : b ≤ 0
⊢ Antitone fun a => a / b

Tactic:
intro a a' h'

Result:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ (fun a => a / b) a' ≤ (fun a => a / b) a

Proof state:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a' * b⁻¹ ≤ a * b⁻¹

Tactic:
rw [← neg_neg (a * b⁻¹), ← neg_neg (a' * b⁻¹), neg_le_neg_iff, mul_comm a b⁻¹, mul_comm a' b⁻¹,
  ← neg_mul b⁻¹ a, ← neg_mul b⁻¹ a', mul_comm (-b⁻¹) a, mul_comm (-b⁻¹) a', ← inv_neg b]

Result:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Proof state:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
this : 0 ≤ -b
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Tactic:
exact div_le_div_right_of_nonneg this h'

Result:
no goals
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem ContDiffAt.real_of_complex {n : WithTop ℕ∞} (h : ContDiffAt ℂ n e z) :
    ContDiffAt ℝ n (fun x : ℝ => (e x).re) z

Proof state:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e ↑z
C : ContDiffAt ℝ n re (e ↑z)
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z

Tactic:
exact C.comp z (B.comp z A)

Result:
no goals

Proof state:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z

Tactic:
have C : ContDiffAt ℝ n re (e z) := reCLM.contDiff.contDiffAt

Result:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e ↑z
C : ContDiffAt ℝ n re (e ↑z)
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z

Proof state:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z

Tactic:
have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealCLM.contDiff.contDiffAt

Result:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z

Proof state:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z

Tactic:
have B : ContDiffAt ℝ n e z := h.restrict_scalars ℝ

Result:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem eventually_nhds_prod_iff {f : Filter ι} {x₀ : α} {p : α × ι → Prop} :
    (∀ᶠ x in 𝓝 x₀ ×ˢ f, p x) ↔ ∃ ε > (0 : ℝ), ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧
      ∀ ⦃x⦄, dist x x₀ < ε → ∀ ⦃i⦄, pa i → p (x, i)

Proof state:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Tactic:
refine (nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_

Result:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ i, (0 < i.1 ∧ i.2 ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.1 ×ˢ id i.2 → p x) ↔
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Proof state:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ i, (0 < i.1 ∧ i.2 ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.1 ×ˢ id i.2 → p x) ↔
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Tactic:
simp only [Prod.exists, forall_prod_set, id, mem_ball, and_assoc, exists_and_left, and_imp]

Result:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ a, 0 < a ∧ ∃ x ∈ f, ∀ (x_1 : α), dist x_1 x₀ < a → ∀ y ∈ x, p (x_1, y)) ↔
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Proof state:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ a, 0 < a ∧ ∃ x ∈ f, ∀ (x_1 : α), dist x_1 x₀ < a → ∀ y ∈ x, p (x_1, y)) ↔
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
lemma Polynomial.Monic.quotient_isIntegralElem {g : S[X]} (mon : g.Monic) {I : Ideal S[X]}
    (h : g ∈ I) :
    ((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem (Ideal.Quotient.mk I X)

Proof state:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ eval₂ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) ((Ideal.Quotient.mk I) X) g = 0

Tactic:
rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]

Result:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) g

Proof state:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) (∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i) * X ^ i)

Tactic:
simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]

Result:
no goals

Proof state:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem ((Ideal.Quotient.mk I) X)

Tactic:
exact ⟨g, mon, by
rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
nth_rw 3 [(as_sum_range_C_mul_X_pow g)]
simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]⟩

Result:
no goals

Proof state:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) g

Tactic:
nth_rw 3 [(as_sum_range_C_mul_X_pow g)]

Result:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) (∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i) * X ^ i)
-- Mathlib/Data/Nat/Factorization/Basic.lean
lemma factorizationLCMRight_pos :
    0 < factorizationLCMRight a b

Proof state:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H

Result:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
H : p = 0 ∧ ¬(a.lcm b).factorization p = 0
⊢ False

Proof state:
case a
a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then 1 else i ^ (a.lcm b).factorization i) ≠ 0

Tactic:
intro p _ H

Result:
case a
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
⊢ False

Proof state:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

Tactic:
simp only [h, reduceIte, pow_eq_zero_iff', ne_eq, reduceCtorEq] at H

Result:
no goals

Proof state:
case a
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
⊢ False

Tactic:
by_cases h : b.factorization p ≤ a.factorization p

Result:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Proof state:
case a
a b : ℕ
⊢ a.factorizationLCMRight b ≠ 0

Tactic:
rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]

Result:
case a
a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then 1 else i ^ (a.lcm b).factorization i) ≠ 0

Proof state:
a b : ℕ
⊢ 0 < a.factorizationLCMRight b

Tactic:
apply Nat.pos_of_ne_zero

Result:
case a
a b : ℕ
⊢ a.factorizationLCMRight b ≠ 0

Proof state:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
H : p = 0 ∧ ¬(a.lcm b).factorization p = 0
⊢ False

Tactic:
simpa [H.1] using H.2

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem gcd_fib_add_self (m n : ℕ) : gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)

Proof state:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))

Tactic:
rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]

Result:
no goals

Proof state:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))

Tactic:
ring_nf

Result:
no goals

Proof state:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))

Tactic:
rw [← fib_add n.pred _]

Result:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))

Proof state:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
rw [← h, succ_eq_add_one]

Result:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))

Proof state:
case inl
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | h

Result:
case inl
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)

case inr
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Proof state:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))

Tactic:
calc
  gcd (fib m) (fib (n.pred + 1 + m)) =
      gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) := by
      rw [← fib_add n.pred _]
      ring_nf
  _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
      rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
  _ = gcd (fib m) (fib (n.pred + 1)) :=
    Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))

Result:
no goals

Proof state:
case inr
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
replace h := Nat.succ_pred_eq_of_pos h

Result:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem left_of_comp {g : α → α} (hco : Commute f g) (hfg : IsPeriodicPt (f ∘ g) n x)
    (hg : IsPeriodicPt g n x) : IsPeriodicPt f n x

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
exact hfg.left_of_comp hg

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
rw [IsPeriodicPt, hco.comp_iterate] at hfg

Result:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/RArray.lean
theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) :
    (ofFn f h).get i = f i :=
  go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2
where
  go lb ub h1 h2 (h3 : lb ≤ i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i

Proof state:
case e_a.e_val
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
h3✝ : lb✝ ≤ ↑i
h3 : ↑i < lb✝ + 1
⊢ lb✝ = ↑i

Tactic:
omega

Result:
no goals

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
h3✝ : lb✝ ≤ ↑i
h3 : ↑i < lb✝ + 1
⊢ f ⟨lb✝, ⋯⟩ = f i

Tactic:
congr

Result:
case e_a.e_val
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
h3✝ : lb✝ ≤ ↑i
h3 : ↑i < lb✝ + 1
⊢ lb✝ = ↑i
-- Mathlib/Algebra/QuaternionBasis.lean
theorem lift_add (x y : ℍ[R,c₁,c₂,c₃]) : q.lift (x + y) = q.lift x + q.lift y

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (algebraMap R A) x.re + (algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      ((algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x + y) = q.lift x + q.lift y

Tactic:
simp only [lift, add_re, map_add, add_imI, add_smul, add_imJ, add_imK]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (algebraMap R A) x.re + (algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      ((algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)