harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem residue_eq_zero_iff_sMod_eq_zero (p : ℕ) (w : 1 < p) :
    lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0

Proof state:
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0

Tactic:
simp? [ZMod.intCast_zmod_eq_zero_iff_dvd] at h says
  simp only [ZMod.intCast_zmod_eq_zero_iff_dvd, ofNat_pos, pow_pos, cast_pred,
    cast_pow, cast_ofNat] at h

Result:
case mp
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) = 0

Proof state:
case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0

Tactic:
simp only [ZMod.intCast_zmod_eq_zero_iff_dvd, ofNat_pos, pow_pos, cast_pred,
  cast_pow, cast_ofNat] at h

Result:
case mp
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) = 0

Proof state:
p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0

Tactic:
rw [sZMod_eq_sMod p]

Result:
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0

Proof state:
case mp
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) = 0

Tactic:
apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h <;> clear h

Result:
p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)

p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1

Proof state:
p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)

Tactic:
exact sMod_nonneg _ (by positivity) _

Result:
no goals

Proof state:
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1

Tactic:
exact sMod_lt _ (by positivity) _

Result:
no goals

Proof state:
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑(sMod p (p - 2)) = 0

Tactic:
rw [h]

Result:
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑0 = 0

Proof state:
case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0

Tactic:
intro h

Result:
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑(sMod p (p - 2)) = 0

Proof state:
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0

Tactic:
constructor

Result:
case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0

case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0

Proof state:
case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0

Tactic:
intro h

Result:
case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0

Proof state:
p : ℕ
w : 1 < p
⊢ p ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
p : ℕ
w : 1 < p
⊢ lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0

Tactic:
dsimp [lucasLehmerResidue]

Result:
p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
-- Mathlib/Data/Nat/Bits.lean
@[simp]
lemma div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n)

Proof state:
n : ℕ
⊢ (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2

Tactic:
simp only [bodd, boddDiv2, div2]

Result:
n : ℕ
⊢ (match n.boddDiv2 with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)).snd =
    bif n.boddDiv2.fst then n.boddDiv2.snd.succ else n.boddDiv2.snd

Proof state:
n : ℕ
⊢ (match n.boddDiv2 with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)).snd =
    bif n.boddDiv2.fst then n.boddDiv2.snd.succ else n.boddDiv2.snd

Tactic:
rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem exists_hasEigenvalue_of_genEigenspace_eq_top [Nontrivial M] {f : End R M} (k : ℕ∞)
    (hf : ⨆ μ, f.genEigenspace μ k = ⊤) :
    ∃ μ, f.HasEigenvalue μ

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ ∃ μ, f.HasEigenvalue μ

Tactic:
suffices ∃ μ, f.HasUnifEigenvalue μ k by
  peel this with μ hμ
  exact HasUnifEigenvalue.lt zero_lt_one hμ

Result:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ ∃ μ, f.HasUnifEigenvalue μ k

Proof state:
case h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : ∃ μ, f.HasUnifEigenvalue μ k
μ : R
hμ : f.HasUnifEigenvalue μ k
⊢ f.HasEigenvalue μ

Tactic:
exact HasUnifEigenvalue.lt zero_lt_one hμ

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : ∃ μ, f.HasUnifEigenvalue μ k
⊢ ∃ μ, f.HasEigenvalue μ

Tactic:
peel this with μ hμ

Result:
case h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : ∃ μ, f.HasUnifEigenvalue μ k
μ : R
hμ : f.HasUnifEigenvalue μ k
⊢ f.HasEigenvalue μ

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ ∃ μ, f.HasUnifEigenvalue μ k

Tactic:
simp [HasUnifEigenvalue, ← not_forall, ← iSup_eq_bot, hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
    (input : RefVec aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
    [LawfulOperator α Ref f] [LawfulMapOperator α f] :
    ∀ (idx : Nat) (hidx : idx < curr),
      (go aig curr hcurr s input f).vec.get idx (by omega)
        =
      (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig curr hcurr s input f).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig curr hcurr s input f).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig curr hcurr s input f).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig curr hcurr s input f).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx : idx < curr
⊢ idx < len

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_ratCast_iff_of_nonneg {q : ℚ} (hq : 0 ≤ q) :
    Irrational (√q) ↔ ¬IsSquare q

Proof state:
case mp.intro
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ∃ r, q = r * r

Tactic:
refine ⟨y, Rat.cast_injective (α := ℝ) ?_⟩

Result:
case mp.intro
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ↑q = ↑(y * y)

Proof state:
case mpr
q : ℚ
hq : 0 ≤ q
⊢ (∃ r, q = r * r) → ∃ y, ↑y = √↑q

Tactic:
rintro ⟨q', rfl⟩

Result:
case mpr.intro
q' : ℚ
hq : 0 ≤ q' * q'
⊢ ∃ y, ↑y = √↑(q' * q')

Proof state:
case mp
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) → ∃ r, q = r * r

Tactic:
rintro ⟨y, hy⟩

Result:
case mp.intro
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ∃ r, q = r * r

Proof state:
q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q

Tactic:
refine Iff.not (?_ : Exists _ ↔ Exists _)

Result:
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) ↔ ∃ r, q = r * r

Proof state:
case mp.intro
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ↑q = ↑(y * y)

Tactic:
rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]

Result:
no goals

Proof state:
case mpr.intro
q' : ℚ
hq : 0 ≤ q' * q'
⊢ ∃ y, ↑y = √↑(q' * q')

Tactic:
exact ⟨|q'|, mod_cast (sqrt_mul_self_eq_abs q').symm⟩

Result:
no goals

Proof state:
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) ↔ ∃ r, q = r * r

Tactic:
constructor

Result:
case mp
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) → ∃ r, q = r * r

case mpr
q : ℚ
hq : 0 ≤ q
⊢ (∃ r, q = r * r) → ∃ y, ↑y = √↑q
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem IsLimit.aleph0_le {c : Cardinal} (h : IsLimit c) : ℵ₀ ≤ c

Proof state:
case intro
n : ℕ
h : (↑n).IsLimit
h' : ↑n < ℵ₀
⊢ False

Tactic:
exact not_isLimit_natCast n h

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : c.IsLimit
h' : c < ℵ₀
⊢ False

Tactic:
rcases lt_aleph0.1 h' with ⟨n, rfl⟩

Result:
case intro
n : ℕ
h : (↑n).IsLimit
h' : ↑n < ℵ₀
⊢ False

Proof state:
c : Cardinal.{u_1}
h : c.IsLimit
⊢ ℵ₀ ≤ c

Tactic:
by_contra! h'

Result:
c : Cardinal.{u_1}
h : c.IsLimit
h' : c < ℵ₀
⊢ False
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem inner_eq_neg_mul_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) :
    ⟪x, y⟫ = -(‖x‖ * ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ inner x y = -(‖x‖ * ‖y‖)

Tactic:
simp [← cos_angle_mul_norm_mul_norm, h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_smul_right (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g

Proof state:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
r : R
f : M →ₗ[R] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map f (r • g))) x✝¹) x✝ = (((mk R M N).compr₂ (r • map f g)) x✝¹) x✝

Tactic:
simp only [smul_tmul, compr₂_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
r : R
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ map f (r • g) = r • map f g

Tactic:
ext

Result:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
r : R
f : M →ₗ[R] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map f (r • g))) x✝¹) x✝ = (((mk R M N).compr₂ (r • map f g)) x✝¹) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem lemma_congr (x x' : Bool) (h1 : x' = x) (h2 : x = true) : x' = true

Proof state:
x x' : Bool
h1 : x' = x
h2 : x = true
⊢ x' = true

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem one_lt_finprod' {M : Type*} [OrderedCancelCommMonoid M] {f : ι → M}
    (h : ∀ i, 1 ≤ f i) (h' : ∃ i, 1 < f i) (hf : (mulSupport f).Finite) : 1 < ∏ᶠ i, f i

Proof state:
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : (mulSupport f).Finite
⊢ 1 < ∏ᶠ (i : ι), f i

Tactic:
rcases h' with ⟨i, hi⟩

Result:
case intro
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : (mulSupport f).Finite
i : ι
hi : 1 < f i
⊢ 1 < ∏ᶠ (i : ι), f i

Proof state:
case intro
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : (mulSupport f).Finite
i : ι
hi : 1 < f i
⊢ 1 < ∏ i ∈ hf.toFinset, f i

Tactic:
refine Finset.one_lt_prod' (fun i _ ↦ h i) ⟨i, ?_, hi⟩

Result:
case intro
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : (mulSupport f).Finite
i : ι
hi : 1 < f i
⊢ i ∈ hf.toFinset

Proof state:
case intro
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : (mulSupport f).Finite
i : ι
hi : 1 < f i
⊢ i ∈ hf.toFinset

Tactic:
simpa only [Finite.mem_toFinset, mem_mulSupport] using ne_of_gt hi

Result:
no goals

Proof state:
case intro
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : (mulSupport f).Finite
i : ι
hi : 1 < f i
⊢ 1 < ∏ᶠ (i : ι), f i

Tactic:
rw [finprod_eq_prod _ hf]

Result:
case intro
ι : Type u_3
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : (mulSupport f).Finite
i : ι
hi : 1 < f i
⊢ 1 < ∏ i ∈ hf.toFinset, f i
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_add_mul {A : Matrix m m α} (U : Matrix m n α)
    (V : Matrix n m α) (hA : IsUnit A.det) :
    (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Tactic:
nth_rewrite 1 [← Matrix.mul_one A]

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Tactic:
rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
  det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b)
    (h : lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a

Proof state:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ lfpApprox f x b ≤ lfpApprox f x a

Tactic:
conv => left; rw [lfpApprox]

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ sSup ({x_1 | ∃ b_1, ∃ (_ : b_1 < b), f (lfpApprox f x b_1) = x_1} ∪ {x}) ≤ lfpApprox f x a

Proof state:
case h.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ x ≤ lfpApprox f x a ∧ ∀ a_1 < b, f (lfpApprox f x a_1) ≤ lfpApprox f x a

Tactic:
apply And.intro (le_lfpApprox f x)

Result:
case h.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ ∀ a_1 < b, f (lfpApprox f x a_1) ≤ lfpApprox f x a
-- Mathlib/Algebra/Module/Bimodule.lean
theorem smul_mem (p : Submodule (A ⊗[R] B) M) (a : A) {m : M} (hm : m ∈ p) : a • m ∈ p

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
this : a • m = a ⊗ₜ[R] 1 • m
⊢ a • m ∈ p

Tactic:
exact this.symm ▸ p.smul_mem _ hm

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p

Tactic:
suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm

Result:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m = a ⊗ₜ[R] 1 • m

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m = a ⊗ₜ[R] 1 • m

Tactic:
simp [TensorProduct.Algebra.smul_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracketWithin_add_right (hW : DifferentiableWithinAt 𝕜 W s x)
    (hW₁ : DifferentiableWithinAt 𝕜 W₁ s x) (hs :  UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 V (W + W₁) s x =
      lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 V (W + W₁) s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 (W + W₁) s x) (V x) - ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 (W + W₁) s x) (V x) - ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))

Tactic:
rw [fderivWithin_add' hs hW hW₁, ContinuousLinearMap.add_apply]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W₁ s x) (V x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W₁ s x) (V x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))

Tactic:
abel

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem map {f : A →ₐ[R] A'} (hf_inj : Set.InjOn f (adjoin R (range x))) :
    AlgebraicIndependent R (f ∘ x)

Proof state:
case hf
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x✝ : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x✝))
this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)
h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range
x y : MvPolynomial ι R
hxy : (f.comp (aeval x✝)) x = (f.comp (aeval x✝)) y
⊢ x = y

Tactic:
rw [adjoin_eq_range] at hf_inj

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x✝ : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(aeval Subtype.val).range
this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)
h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range
x y : MvPolynomial ι R
hxy : (f.comp (aeval x✝)) x = (f.comp (aeval x✝)) y
⊢ x = y
-- Mathlib/Data/Set/Accumulate.lean
theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x

Proof state:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i

Tactic:
intro z x x' ⟨_, hz⟩

Result:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i

Proof state:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, Accumulate s x ⊆ ⋃ x, s x

Tactic:
simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]

Result:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, Accumulate s x = ⋃ x, s x

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, Accumulate s x ⊆ ⋃ x, s x

case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, Accumulate s x

Proof state:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, Accumulate s x

Tactic:
exact iUnion_mono fun i => subset_accumulate

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i

Tactic:
exact ⟨x', hz⟩

Result:
no goals