harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal]
    (P : (factors (map (algebraMap R S) p)).toFinset) :
    finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P) =
      ramificationIdx (algebraMap R S) p P * inertiaDeg p (P : Ideal S)

Proof state:
case hP0
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : p.IsMaximal
P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }
⊢ ↑P ≠ ⊥

case he
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : p.IsMaximal
P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }
⊢ ramificationIdx (algebraMap R S) p ↑P ≠ 0

Tactic:
exacts [Factors.ne_bot p P, NeZero.ne _]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : p.IsMaximal
P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }
⊢ finrank (R ⧸ p) (S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P) =
    ramificationIdx (algebraMap R S) p ↑P * p.inertiaDeg ↑P

Tactic:
rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]

Result:
case hP0
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : p.IsMaximal
P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }
⊢ ↑P ≠ ⊥

case he
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : p.IsMaximal
P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }
⊢ ramificationIdx (algebraMap R S) p ↑P ≠ 0
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.isOpen_iff (s : Set M) :
    IsOpen s ↔ ∀ x : M, IsOpen <| chartAt H x '' ((chartAt H x).source ∩ s)

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
⊢ IsOpen s ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))

Tactic:
rw [isOpen_iff_of_cover (fun i ↦ (chartAt H i).open_source) (iUnion_source_chartAt H M)]

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
⊢ (∀ (i : M), IsOpen ((chartAt H i).source ∩ s)) ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
⊢ (∀ (i : M), IsOpen ((chartAt H i).source ∩ s)) ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))

Tactic:
simp only [(chartAt H _).isOpen_image_iff_of_subset_source inter_subset_left]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma polynomial_eq : W'.polynomial = Cubic.toPoly
    ⟨0, 1, Cubic.toPoly ⟨0, 0, W'.a₁, W'.a₃⟩, Cubic.toPoly ⟨-1, -W'.a₂, -W'.a₄, -W'.a₆⟩⟩

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    C 0 * Y ^ 3 + C 1 * Y ^ 2 + C (C 0 * X ^ 3 + C 0 * X ^ 2 + C W'.a₁ * X + C W'.a₃) * Y +
      C (C (-1) * X ^ 3 + C (-W'.a₂) * X ^ 2 + C (-W'.a₄) * X + C (-W'.a₆))

Tactic:
C_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y ^ 2 + (C (C W'.a₁) * C X + C (C W'.a₃)) * Y - (C X ^ 3 + C (C W'.a₂) * C X ^ 2 + C (C W'.a₄) * C X + C (C W'.a₆)) =
    0 * Y ^ 3 + 1 * Y ^ 2 + (0 * C X ^ 3 + 0 * C X ^ 2 + C (C W'.a₁) * C X + C (C W'.a₃)) * Y +
      (-1 * C X ^ 3 + -C (C W'.a₂) * C X ^ 2 + -C (C W'.a₄) * C X + -C (C W'.a₆))

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y ^ 2 + (C (C W'.a₁) * C X + C (C W'.a₃)) * Y - (C X ^ 3 + C (C W'.a₂) * C X ^ 2 + C (C W'.a₄) * C X + C (C W'.a₆)) =
    0 * Y ^ 3 + 1 * Y ^ 2 + (0 * C X ^ 3 + 0 * C X ^ 2 + C (C W'.a₁) * C X + C (C W'.a₃)) * Y +
      (-1 * C X ^ 3 + -C (C W'.a₂) * C X ^ 2 + -C (C W'.a₄) * C X + -C (C W'.a₆))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ W'.polynomial =
    { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
        d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly

Tactic:
simp only [polynomial, Cubic.toPoly]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    C 0 * Y ^ 3 + C 1 * Y ^ 2 + C (C 0 * X ^ 3 + C 0 * X ^ 2 + C W'.a₁ * X + C W'.a₃) * Y +
      C (C (-1) * X ^ 3 + C (-W'.a₂) * X ^ 2 + C (-W'.a₄) * X + C (-W'.a₆))
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma not_nil_of_adj_toSubgraph {u v} {x : V} {p : G.Walk u v} (hadj : p.toSubgraph.Adj w x) :
    ¬p.Nil

Proof state:
V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
⊢ ¬p.Nil

Tactic:
cases p <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_congr {g : α → ℝ} (hfg : f =ᵐ[μ] g) :
    μ.tilted f = μ.tilted g

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ rexp (f x) = rexp (g x)

Tactic:
rw [hx]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
⊢ μ.tilted f = μ.tilted g

Tactic:
refine withDensity_congr_ae ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
⊢ (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =ᶠ[ae μ] fun x =>
    ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ μ.tilted f = μ.tilted g

Tactic:
have h_int_eq : ∫ x, exp (f x) ∂μ = ∫ x, exp (g x) ∂μ := by
  refine integral_congr_ae ?_
  filter_upwards [hfg] with x hx
  rw [hx]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
⊢ μ.tilted f = μ.tilted g

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ (fun x => rexp (f x)) =ᶠ[ae μ] fun x => rexp (g x)

Tactic:
filter_upwards [hfg] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ rexp (f x) = rexp (g x)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
⊢ (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =ᶠ[ae μ] fun x =>
    ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)

Tactic:
filter_upwards [hfg] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
x : α
hx : f x = g x
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ

Tactic:
refine integral_congr_ae ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ (fun x => rexp (f x)) =ᶠ[ae μ] fun x => rexp (g x)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ
x : α
hx : f x = g x
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)

Tactic:
rw [h_int_eq, hx]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem smul_coe : x • (y : ℍ[R,c₁,c₂,c₃]) = ↑(x * y)

Proof state:
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ x • ↑y = ↑(x * y)

Tactic:
rw [coe_mul, coe_mul_eq_smul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem eventually_constant_prod {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
    (∏ k ∈ range n, u k) = ∏ k ∈ range N, u k

Proof state:
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
n : ℕ
hn : N ≤ n
⊢ ∏ k ∈ range n, u k = ∏ k ∈ range N, u k

Tactic:
obtain ⟨m, rfl : n = N + m⟩ := Nat.exists_eq_add_of_le hn

Result:
case intro
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
hn : N ≤ N + m
⊢ ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k

Proof state:
case intro.succ
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
hm : ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k
⊢ ∏ k ∈ range (N + (m + 1)), u k = ∏ k ∈ range N, u k

Tactic:
simp [← add_assoc, prod_range_succ, hm, hu]

Result:
no goals

Proof state:
case intro.zero
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
⊢ ∏ k ∈ range (N + 0), u k = ∏ k ∈ range N, u k

Tactic:
simp

Result:
no goals

Proof state:
case intro
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
hn : N ≤ N + m
⊢ ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k

Tactic:
clear hn

Result:
case intro
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
⊢ ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k

Proof state:
case intro
β : Type u_4
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
⊢ ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k

Tactic:
induction m with
| zero => simp
| succ m hm => simp [← add_assoc, prod_range_succ, hm, hu]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem exists_hasDerivAt_eq_slope : ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)

Proof state:
case intro.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)

Tactic:
use c, cmem

Result:
case right
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)

Proof state:
case right
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)

Tactic:
rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc

Result:
no goals

Proof state:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)

Tactic:
obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Ioo a b, (b - a) * f' c = (f b - f a) * 1 :=
  exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' id 1 continuousOn_id
    fun x _ => hasDerivAt_id x

Result:
case intro.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
-- Mathlib/RingTheory/RingHom/Finite.lean
theorem finite_respectsIso : RespectsIso @Finite

Proof state:
⊢ RespectsIso @Finite

Tactic:
apply finite_stableUnderComposition.respectsIso

Result:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Finite

Proof state:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Finite

Tactic:
intros

Result:
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e✝ : R✝ ≃+* S✝
⊢ e✝.toRingHom.Finite

Proof state:
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e✝ : R✝ ≃+* S✝
⊢ e✝.toRingHom.Finite

Tactic:
exact Finite.of_surjective _ (RingEquiv.toEquiv _).surjective

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^ n
  | 0 => by simp
  | n + 1 => by simpa only [pow_succ']
      using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_nonneg ha _) (ha.trans hab)

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
n : ℕ
⊢ a ^ (n + 1) ≤ b ^ (n + 1)

Tactic:
simpa only [pow_succ']
using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_nonneg ha _) (ha.trans hab)

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ 0 ≤ b ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem sq_le_two_pow_add_one_minus_three (n : ℕ) : n ^ 2 ≤ 2 ^ (n + 1) - 3

Proof state:
case succ.zero
hk : 0 ^ 2 ≤ 2 ^ (0 + 1) - 3
⊢ (0 + 1) ^ 2 ≤ 2 ^ (0 + 1 + 1) - 3

Tactic:
norm_num

Result:
no goals

Proof state:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ (k + 1 + 1) ^ 2 ≤ 2 ^ (k + 1 + 1 + 1) - 3

Tactic:
rw [add_sq, Nat.pow_succ 2, mul_comm _ 2, two_mul (2 ^ _),
    add_tsub_assoc_of_le, add_comm (2 ^ _), add_assoc]

Result:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ (k + 1) ^ 2 + (2 * (k + 1) * 1 + 1 ^ 2) ≤ 2 ^ (k + 2) - 3 + 2 ^ (k + 2)

case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 3 ≤ 2 ^ (k + 2)

Proof state:
case zero

⊢ 0 ^ 2 ≤ 2 ^ (0 + 1) - 3

Tactic:
norm_num

Result:
no goals

Proof state:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 2 * (k + 1) < 2 ^ (k + 2)

Tactic:
rw [Nat.pow_succ, mul_comm _ 2, mul_lt_mul_left (zero_lt_two' ℕ)]

Result:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ k + 1 < 2 ^ (k + 1)

Proof state:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 3 ≤ 2 ^ k * 2 * 2

Tactic:
linarith [one_le_pow k 2 zero_lt_two]

Result:
no goals

Proof state:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ k + 1 < 2 ^ (k + 1)

Tactic:
exact Nat.lt_two_pow_self

Result:
no goals

Proof state:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 2 * (k + 1) + 1 ≤ 2 ^ (k + 2)

Tactic:
apply succ_le_of_lt

Result:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 2 * (k + 1) < 2 ^ (k + 2)

Proof state:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 2 * (k + 1) * 1 + 1 ^ 2 ≤ 2 ^ (k + 2)

Tactic:
norm_num

Result:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 2 * (k + 1) + 1 ≤ 2 ^ (k + 2)

Proof state:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ (k + 1) ^ 2 + (2 * (k + 1) * 1 + 1 ^ 2) ≤ 2 ^ (k + 2) - 3 + 2 ^ (k + 2)

Tactic:
apply Nat.add_le_add hk

Result:
case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 2 * (k + 1) * 1 + 1 ^ 2 ≤ 2 ^ (k + 2)

Proof state:
n : ℕ
⊢ n ^ 2 ≤ 2 ^ (n + 1) - 3

Tactic:
induction' n with k hk

Result:
case zero

⊢ 0 ^ 2 ≤ 2 ^ (0 + 1) - 3

case succ
k : ℕ
hk : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3

Proof state:
case succ
k : ℕ
hk : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3

Tactic:
rcases k with - | k

Result:
case succ.zero
hk : 0 ^ 2 ≤ 2 ^ (0 + 1) - 3
⊢ (0 + 1) ^ 2 ≤ 2 ^ (0 + 1 + 1) - 3

case succ.succ
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ (k + 1 + 1) ^ 2 ≤ 2 ^ (k + 1 + 1 + 1) - 3

Proof state:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 3 ≤ 2 ^ (k + 2)

Tactic:
rw [Nat.pow_succ, Nat.pow_succ]

Result:
case succ.succ.h
k : ℕ
hk : (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3
⊢ 3 ≤ 2 ^ k * 2 * 2
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem eq_of_has_deriv_right_eq (derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x)
    (derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x) (fcont : ContinuousOn f (Icc a b))
    (gcont : ContinuousOn g (Icc a b)) (hi : f a = g a) : ∀ y ∈ Icc a b, f y = g y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
⊢ ∀ y ∈ Icc a b, f y - g y = 0

Tactic:
exact hi ▸ constant_of_has_deriv_right_zero (fcont.sub gcont) fun y hy => by
  simpa only [sub_self] using (derivf y hy).sub (derivg y hy)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a = g a
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
simp only [← @sub_eq_zero _ _ (f _)] at hi ⊢

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
⊢ ∀ y ∈ Icc a b, f y - g y = 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
y : ℝ
hy : y ∈ Ico a b
⊢ HasDerivWithinAt (fun y => f y - g y) 0 (Ici y) y

Tactic:
simpa only [sub_self] using (derivf y hy).sub (derivg y hy)

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem map_modByMonic (h : IsAdjoinRootMonic S f) (g : R[X]) : h.map (g %ₘ f) = h.map g

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ h.map (g %ₘ f) = h.map g

Tactic:
rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div _ h.Monic, sub_right_comm,
  sub_self, zero_sub, dvd_neg]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ f * (g /ₘ f)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ f * (g /ₘ f)

Tactic:
exact ⟨_, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma toAlgHom_comp_sectionOfRetractionKerToTensorAux :
    (IsScalarTower.toAlgHom R P S).comp
      (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id _ _

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
⊢ (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id R S

Tactic:
ext x

Result:
case H
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
x : S
⊢ ((IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf')) x = (AlgHom.id R S) x

Proof state:
case H.intro
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
x : P
⊢ ((IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf')) ((algebraMap P S) x) =
    (AlgHom.id R S) ((algebraMap P S) x)

Tactic:
simp [sectionOfRetractionKerToTensorAux_algebraMap, RingHom.mem_ker.mp]

Result:
no goals

Proof state:
case H
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
x : S
⊢ ((IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf')) x = (AlgHom.id R S) x

Tactic:
obtain ⟨x, rfl⟩ := hf x

Result:
case H.intro
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
x : P
⊢ ((IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf')) ((algebraMap P S) x) =
    (AlgHom.id R S) ((algebraMap P S) x)
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem star_mem_star_iff (S : Subalgebra R A) (x : A) : star x ∈ star S ↔ x ∈ S

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : Subalgebra R A
x : A
⊢ star x ∈ star S ↔ x ∈ S

Tactic:
simp

Result:
no goals