harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : List α) (init : γ) :
    (l.filterMap f).foldrM g init =
      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
init : γ
⊢ foldrM g init (filterMap f []) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init []

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
l : List α
init : γ
⊢ foldrM g init (filterMap f l) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filterMap_cons, foldrM_cons]
  cases f a <;> simp [ih]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldrM g init (filterMap f l) =
      foldrM
        (fun x y =>
          match f x with
          | some b => g b y
          | none => pure y)
        init l
init : γ
⊢ foldrM g init (filterMap f (a :: l)) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init (a :: l)

Tactic:
simp only [filterMap_cons, foldrM_cons]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldrM g init (filterMap f l) =
      foldrM
        (fun x y =>
          match f x with
          | some b => g b y
          | none => pure y)
        init l
init : γ
⊢ foldrM g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    do
    let y ←
      foldrM
          (fun x y =>
            match f x with
            | some b => g b y
            | none => pure y)
          init l
    match f a with
      | some b => g b y
      | none => pure y

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldrM g init (filterMap f l) =
      foldrM
        (fun x y =>
          match f x with
          | some b => g b y
          | none => pure y)
        init l
init : γ
⊢ foldrM g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    do
    let y ←
      foldrM
          (fun x y =>
            match f x with
            | some b => g b y
            | none => pure y)
          init l
    match f a with
      | some b => g b y
      | none => pure y

Tactic:
cases f a <;> simp [ih]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.dvd_iff_eq {p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ p ↔ p = a

Proof state:
case intro
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a

Tactic:
rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)

Result:
case intro.inl.intro
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a

case intro.inr.intro
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1

Proof state:
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ p = a → a ∣ p

Tactic:
rintro rfl

Result:
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p

Proof state:
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a

Tactic:
refine ⟨?_, by rintro rfl; rfl⟩

Result:
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a

Proof state:
case intro.inr.intro
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1

Tactic:
exact (a1 rfl).elim

Result:
no goals

Proof state:
case intro.inl.intro
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a

Tactic:
exact mul_one _

Result:
no goals

Proof state:
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a

Tactic:
rintro ⟨j, rfl⟩

Result:
case intro
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a

Proof state:
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p

Tactic:
rfl

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_add {b₁ b₂ : ℕ} {d : R}
    (_ : a ^ b₁ = c₁) (_ : a ^ b₂ = c₂) (_ : c₁ * c₂ = d) : (a : R) ^ (b₁ + b₂) = d

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a c₁ c₂ : R
b₁ b₂ : ℕ
d : R
x✝² : a ^ b₁ = c₁
x✝¹ : a ^ b₂ = c₂
x✝ : c₁ * c₂ = d
⊢ a ^ (b₁ + b₂) = d

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a : R
b₁ b₂ : ℕ
⊢ a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
b₁ b₂ : ℕ
⊢ a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂

Tactic:
simp [_root_.pow_add]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translate_zpow (x : ℝ) (n : ℤ) :
    translate (Multiplicative.ofAdd x) ^ n = translate (Multiplicative.ofAdd <| ↑n * x)

Proof state:
x : ℝ
n : ℤ
⊢ translate (Multiplicative.ofAdd x) ^ n = translate (Multiplicative.ofAdd (↑n * x))

Tactic:
simp only [← zsmul_eq_mul, ofAdd_zsmul, MonoidHom.map_zpow]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableAtFilter.sub {f g : α → E}
    (hf : IntegrableAtFilter f l μ) (hg : IntegrableAtFilter g l μ) :
    IntegrableAtFilter (f - g) l μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f + -g) l μ

Tactic:
exact hf.add hg.neg

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f - g) l μ

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f + -g) l μ
-- Mathlib/Data/ENNReal/Inv.lean
lemma biSup_add_biSup_le' {p : ι → Prop} {q : κ → Prop} (hp : ∃ i, p i) (hq : ∃ j, q j)
    {g : κ → ℝ≥0∞} (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) :
    (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem inf_covBy_of_covBy_sup_of_covBy_sup_right : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

Tactic:
rw [sup_comm, inf_comm]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ b ⊔ a → b ⋖ b ⊔ a → b ⊓ a ⋖ b

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ b ⊔ a → b ⋖ b ⊔ a → b ⊓ a ⋖ b

Tactic:
exact fun ha hb => inf_covBy_of_covBy_sup_of_covBy_sup_left hb ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Perm.lean
theorem Perm.push (x y : α) {l₁ l₂ : Array α} (p : l₁ ~ l₂) :
    (l₁.push x).push y ~ (l₂.push y).push x

Proof state:
case mk.mk
α : Type u_1
x y : α
toList✝¹ toList✝ : List α
p : toList✝¹ ~ toList✝
⊢ ({ toList := toList✝¹ }.push x).push y ~ ({ toList := toList✝ }.push y).push x

Tactic:
simp only [push_toArray, List.append_assoc, singleton_append, perm_toArray]

Result:
case mk.mk
α : Type u_1
x y : α
toList✝¹ toList✝ : List α
p : toList✝¹ ~ toList✝
⊢ toList✝¹ ++ [x, y] ~ toList✝ ++ [y, x]

Proof state:
α : Type u_1
x y : α
l₁ l₂ : Array α
p : l₁ ~ l₂
⊢ (l₁.push x).push y ~ (l₂.push y).push x

Tactic:
cases l₁

Result:
case mk
α : Type u_1
x y : α
l₂ : Array α
toList✝ : List α
p : { toList := toList✝ } ~ l₂
⊢ ({ toList := toList✝ }.push x).push y ~ (l₂.push y).push x

Proof state:
case mk.mk
α : Type u_1
x y : α
toList✝¹ toList✝ : List α
p : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ ({ toList := toList✝¹ }.push x).push y ~ ({ toList := toList✝ }.push y).push x

Tactic:
simp only [perm_toArray] at p

Result:
case mk.mk
α : Type u_1
x y : α
toList✝¹ toList✝ : List α
p : toList✝¹ ~ toList✝
⊢ ({ toList := toList✝¹ }.push x).push y ~ ({ toList := toList✝ }.push y).push x

Proof state:
case mk
α : Type u_1
x y : α
l₂ : Array α
toList✝ : List α
p : { toList := toList✝ } ~ l₂
⊢ ({ toList := toList✝ }.push x).push y ~ (l₂.push y).push x

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
x y : α
toList✝¹ toList✝ : List α
p : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ ({ toList := toList✝¹ }.push x).push y ~ ({ toList := toList✝ }.push y).push x

Proof state:
case mk.mk
α : Type u_1
x y : α
toList✝¹ toList✝ : List α
p : toList✝¹ ~ toList✝
⊢ toList✝¹ ++ [x, y] ~ toList✝ ++ [y, x]

Tactic:
exact p.append (Perm.swap' _ _ Perm.nil)

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem exists_partition_approximatesLinearOn_of_hasFDerivWithinAt [SecondCountableTopology F]
    (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
    (r : (E →L[ℝ] F) → ℝ≥0) (rpos : ∀ A, r A ≠ 0) :
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
      Pairwise (Disjoint on t) ∧
        (∀ n, MeasurableSet (t n)) ∧
          (s ⊆ ⋃ n, t n) ∧
            (∀ n, ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
              (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y)

Proof state:
case intro.intro.intro.intro.intro.refine_1
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ s ⊆ ⋃ n, disjointed t n

Tactic:
rw [iUnion_disjointed]

Result:
case intro.intro.intro.intro.intro.refine_1
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ s ⊆ ⋃ i, t i

Proof state:
case intro.intro.intro.intro.intro.refine_1
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ s ⊆ ⋃ i, t i

Tactic:
exact st

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_node' (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (node' l x r) = node' (dual r) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.node' x r).dual = r.dual.node' x l.dual

Tactic:
simp [node', add_comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem Isometry.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
    (h : Isometry f) : Isometry (Completion.extension f) :=
  Isometry.of_dist_eq fun x y => induction_on₂ x y
    (isClosed_eq (by fun_prop) (by fun_prop)) fun _ _ ↦ by
      simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
x✝¹ x✝ : α
⊢ dist (Completion.extension f ↑x✝¹) (Completion.extension f ↑x✝) = dist ↑x✝¹ ↑x✝

Tactic:
simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.1) (Completion.extension f x.2)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist x.1 x.2

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_le_natTrailingDegree (hq : q ≠ 0)
    (hpq : p.trailingDegree ≤ q.trailingDegree) : p.natTrailingDegree ≤ q.natTrailingDegree :=
  ENat.toNat_le_toNat hpq <| by simpa

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q ≠ 0
hpq : p.trailingDegree ≤ q.trailingDegree
⊢ q.trailingDegree ≠ ⊤

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_mul_self_eq_abs (x : ℝ) : √(x * x) = |x|

Proof state:
x : ℝ
⊢ √(x * x) = |x|

Tactic:
rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_le_right_iff_le (h : r < 1) : lineMap a b r ≤ b ↔ a ≤ b :=
  Iff.trans (by rw [lineMap_apply_one]) (lineMap_le_lineMap_iff_of_lt h)

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r : k
h : r < 1
⊢ (lineMap a b) r ≤ b ↔ (lineMap a b) r ≤ (lineMap a b) 1

Tactic:
rw [lineMap_apply_one]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem fst_toProd (x : M ∗ N) : (toProd x).1 = fst x

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = fst x

Tactic:
rw [← fst_comp_toProd]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = ((MonoidHom.fst M N).comp toProd) x

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = ((MonoidHom.fst M N).comp toProd) x

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem minpoly_algebraMap_add_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (algebraMap K L r + x)).Splits (algebraMap K L)

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) (minpoly K ((algebraMap K L) r + x))

Tactic:
simpa only [add_comm] using minpoly_add_algebraMap_splits r g

Result:
no goals
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem toZ_iterate_succ_le (n : ℕ) : toZ i0 (succ^[n] i0) ≤ n

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) ≤ ↑n

Tactic:
rw [toZ_of_ge (le_succ_iterate _ _)]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ ↑(Nat.find ⋯) ≤ ↑n

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_min' _ rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ ↑(Nat.find ⋯) ≤ ↑n

Tactic:
norm_cast

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ Nat.find ⋯ ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} {h} :
    get m a h = getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.WF
a : α
fallback : β
h : a ∈ m
⊢ get m a h = getD m a fallback

Tactic:
simp_to_raw using Raw₀.Const.get_eq_getD

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M}
    (hf : ∀ x ∈ p, f x ∈ p) :
    Injective (f.restrict hf) ↔ Disjoint p (ker f)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ x ∈ p, f x ∈ p
⊢ Injective ⇑(f.restrict hf) ↔ Disjoint p (ker f)

Tactic:
rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
  disjoint_iff]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.induction_on_subset {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α)
    (hs : s.Finite) (empty : motive ∅ finite_empty)
    (insert : ∀ {a t}, a ∈ s → ∀ hts : t ⊆ s, a ∉ t → motive t (hs.subset hts) →
      motive (insert a t) ((hs.subset hts).insert a)) : motive s hs

Proof state:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS✝ : Insert.insert a s ⊆ s✝
haS : a ∈ s✝ ∧ s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Tactic:
exact insert haS.1 haS.2 has (hCs haS.2)

Result:
no goals

Proof state:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS : Insert.insert a s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Tactic:
rw [insert_subset_iff] at haS

Result:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS✝ : Insert.insert a s ⊆ s✝
haS : a ∈ s✝ ∧ s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Proof state:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ ∀ {a : α} {s_1 : Set α},
    a ∉ s_1 →
      ∀ (hs_1 : s_1.Finite),
        (fun t x => ∀ (hts : t ⊆ s), motive t ⋯) s_1 hs_1 →
          (fun t x => ∀ (hts : t ⊆ s), motive t ⋯) (Insert.insert a s_1) ⋯

Tactic:
intro a s has _ hCs haS

Result:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS : Insert.insert a s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Proof state:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ motive s hs

Tactic:
refine Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
  (fun _ => empty) ?_ .rfl

Result:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ ∀ {a : α} {s_1 : Set α},
    a ∉ s_1 →
      ∀ (hs_1 : s_1.Finite),
        (fun t x => ∀ (hts : t ⊆ s), motive t ⋯) s_1 hs_1 →
          (fun t x => ∀ (hts : t ⊆ s), motive t ⋯) (Insert.insert a s_1) ⋯
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem length_le_sum_of_one_le (L : List ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum

Proof state:
case nil
h : ∀ (i : ℕ), i ∈ [] → 1 ≤ i
⊢ [].length ≤ [].sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum

Tactic:
exact Nat.add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

Result:
no goals

Proof state:
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ L.length ≤ L.sum

Tactic:
induction L with
| nil => simp
| cons j L IH =>
  rw [sum_cons, length, add_comm]
  exact Nat.add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

Result:
no goals

Proof state:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ (j :: L).sum

Tactic:
rw [sum_cons, length, add_comm]

Result:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lift_pred (o : Ordinal.{v}) : lift.{u} (pred o) = pred (lift.{u} o)

Proof state:
o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
exact if h : ∃ a, o = succ a then by obtain ⟨a, e⟩ := h; simp only [e, pred_succ, lift_succ]
else by rw [pred_eq_iff_not_succ.2 h, pred_eq_iff_not_succ.2 (mt lift_is_succ.1 h)]

Result:
no goals

Proof state:
case intro
o a : Ordinal.{v}
e : o = succ a
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
simp only [e, pred_succ, lift_succ]

Result:
no goals

Proof state:
o : Ordinal.{v}
h : ¬∃ a, o = succ a
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
rw [pred_eq_iff_not_succ.2 h, pred_eq_iff_not_succ.2 (mt lift_is_succ.1 h)]

Result:
no goals

Proof state:
o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
classical
exact if h : ∃ a, o = succ a then by obtain ⟨a, e⟩ := h; simp only [e, pred_succ, lift_succ]
else by rw [pred_eq_iff_not_succ.2 h, pred_eq_iff_not_succ.2 (mt lift_is_succ.1 h)]

Result:
no goals

Proof state:
o : Ordinal.{v}
h : ∃ a, o = succ a
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
obtain ⟨a, e⟩ := h

Result:
case intro
o a : Ordinal.{v}
e : o = succ a
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred