harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[gcongr]
protected lemma mul_lt_mul (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂

Proof state:
case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
hb₂ : b₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Tactic:
lift a₂ to α using ha₂

Result:
case intro.intro.inr.inr.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
hb₂ : b₂ ≠ ⊤
a₂ : α
ha : ↑a₁ < ↑a₂
⊢ ↑a₁ * ↑b₁ < ↑a₂ * b₂

Proof state:
case intro.intro.inr.inr.intro.intro.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
hb₁ : 0 < b₁
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul ha hb.le hb₁ (zero_le _)

Result:
no goals

Proof state:
case intro.intro.inr.inr.intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ a₂ b₂ : α
ha : a₁ < a₂
hb : 0 < b₂
⊢ a₁ * 0 < a₂ * b₂

Tactic:
rw [mul_zero]

Result:
case intro.intro.inr.inr.intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ a₂ b₂ : α
ha : a₁ < a₂
hb : 0 < b₂
⊢ 0 < a₂ * b₂

Proof state:
case intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₁ b₂ : WithTop α
hb : b₁ < b₂
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
⊢ ↑a₁ * b₁ < a₂ * b₂

Tactic:
lift b₁ to α using hb.lt_top.ne

Result:
case intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Proof state:
case intro.intro.inr.inr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ : α
ha : ↑a₁ < ↑a₂
b₂ : α
hb : ↑b₁ < ↑b₂
⊢ ↑a₁ * ↑b₁ < ↑a₂ * ↑b₂

Tactic:
norm_cast at *

Result:
case intro.intro.inr.inr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem pow_smul_eq_iff_minimalPeriod_dvd {n : ℕ} :
    a ^ n • b = b ↔ minimalPeriod (a • ·) b ∣ n

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod (fun x => a • x) b ∣ n

Tactic:
rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem sub_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a - c = b - d

Proof state:
a b c d : Int
h₁ : a = b
h₂ : c = d
⊢ a - c = b - d

Tactic:
subst h₁

Result:
a c d : Int
h₂ : c = d
⊢ a - c = a - d

Proof state:
a c : Int
⊢ a - c = a - c

Tactic:
rfl

Result:
no goals

Proof state:
a c d : Int
h₂ : c = d
⊢ a - c = a - d

Tactic:
subst h₂

Result:
a c : Int
⊢ a - c = a - c
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem C_injective : Function.Injective (C : R → HahnSeries Γ R)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
⊢ r = s

Tactic:
have h := rs 0

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
h : (C r).coeff 0 = (C s).coeff 0
⊢ r = s

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : C r = C s
⊢ r = s

Tactic:
rw [HahnSeries.ext_iff, funext_iff] at rs

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
⊢ r = s

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
h : (C r).coeff 0 = (C s).coeff 0
⊢ r = s

Tactic:
rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
⊢ Injective ⇑C

Tactic:
intro r s rs

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : C r = C s
⊢ r = s
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem support_cycleOf_eq_nil_iff [DecidableEq α] [Fintype α] :
    (f.cycleOf x).support = ∅ ↔ x ∉ f.support

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (f.cycleOf x).support = ∅ ↔ x ∉ f.support

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Defs.lean
theorem toPNat'_coe : ∀ n : ℕ, (toPNat' n : ℕ) = ite (0 < n) n 1
  | 0 => rfl
  | m + 1 => by
    rw [if_pos (succ_pos m)]
    rfl

Proof state:
m : ℕ
⊢ ↑(m + 1).toPNat' = m + 1

Tactic:
rfl

Result:
no goals

Proof state:
m : ℕ
⊢ ↑(m + 1).toPNat' = if 0 < m + 1 then m + 1 else 1

Tactic:
rw [if_pos (succ_pos m)]

Result:
m : ℕ
⊢ ↑(m + 1).toPNat' = m + 1
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_bot_ae_eq (f : α → E) :
    μ[f|⊥] =ᵐ[μ] fun _ => (μ Set.univ).toReal⁻¹ • ∫ x, f x ∂μ

Proof state:
case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f|⊥] =ᶠ[ae 0] fun x => (0 Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂0

Tactic:
rw [ae_zero]

Result:
case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f|⊥] =ᶠ[⊥] fun x => (0 Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂0

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ μ[f|⊥] =ᶠ[ae μ] fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Result:
case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f|⊥] =ᶠ[ae 0] fun x => (0 Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂0

case inr
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f|⊥] =ᶠ[ae μ] fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case inr
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f|⊥] =ᶠ[ae μ] fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
exact Eventually.of_forall <| congr_fun (condExp_bot' f)

Result:
no goals

Proof state:
case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f|⊥] =ᶠ[⊥] fun x => (0 Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂0

Tactic:
exact eventually_bot

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem comp_lift (g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f)

Proof state:
α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ g.comp (lift f) = lift (⇑g ∘ f)

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
x✝ : α
⊢ (g.comp (lift f)) (of x✝) = (lift (⇑g ∘ f)) (of x✝)

Proof state:
case h
α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
x✝ : α
⊢ (g.comp (lift f)) (of x✝) = (lift (⇑g ∘ f)) (of x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_arrow_eq_zero_iff : #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0

Proof state:
α : Type u
β' : Type v
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0

Tactic:
simp_rw [mk_eq_zero_iff, mk_ne_zero_iff, isEmpty_fun]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtom_iff {s : Set α} : IsAtom s ↔ ∃ x, s = {x}

Proof state:
case intro
α : Type u_2
x : α
⊢ IsAtom {x}

Tactic:
exact isAtom_singleton x

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}

Tactic:
exact
  ⟨x, eq_singleton_iff_unique_mem.2
      ⟨hx, fun y hy => (hs {y} (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩

Result:
no goals

Proof state:
α : Type u_2
s : Set α
⊢ (∃ x, s = {x}) → IsAtom s

Tactic:
rintro ⟨x, rfl⟩

Result:
case intro
α : Type u_2
x : α
⊢ IsAtom {x}

Proof state:
α : Type u_2
s : Set α
⊢ (s.Nonempty ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ x, s = {x}

Tactic:
rintro ⟨⟨x, hx⟩, hs⟩

Result:
case intro.intro
α : Type u_2
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}

Proof state:
α : Type u_2
s : Set α
⊢ IsAtom s → ∃ x, s = {x}

Tactic:
rw [isAtom_iff_le_of_ge, bot_eq_empty, ← nonempty_iff_ne_empty]

Result:
α : Type u_2
s : Set α
⊢ (s.Nonempty ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ x, s = {x}

Proof state:
α : Type u_2
s : Set α
⊢ IsAtom s ↔ ∃ x, s = {x}

Tactic:
refine
  ⟨?_, by
    rintro ⟨x, rfl⟩
    exact isAtom_singleton x⟩

Result:
α : Type u_2
s : Set α
⊢ IsAtom s → ∃ x, s = {x}
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem IsClique.card_le_of_coloring {s : Finset V} (h : G.IsClique s) [Fintype α]
    (C : G.Coloring α) : s.card ≤ Fintype.card α

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
f : ⊤ ↪g G
⊢ s.card ≤ card α

Tactic:
convert Fintype.card_le_of_injective _ (C.comp f.toHom).injective_of_top_hom using 1

Result:
case h.e'_3
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
f : ⊤ ↪g G
⊢ s.card = card ↑↑s

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : G.IsClique ↑s
inst✝ : Fintype α
C : G.Coloring α
⊢ s.card ≤ card α

Tactic:
rw [isClique_iff_induce_eq] at h

Result:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
⊢ s.card ≤ card α

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
f : induce (↑s) G ↪g G
⊢ s.card ≤ card α

Tactic:
rw [h] at f

Result:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
f : ⊤ ↪g G
⊢ s.card ≤ card α

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
⊢ s.card ≤ card α

Tactic:
have f : G.induce ↑s ↪g G := Embedding.comap (Function.Embedding.subtype fun x => x ∈ ↑s) G

Result:
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
f : induce (↑s) G ↪g G
⊢ s.card ≤ card α

Proof state:
case h.e'_3
V : Type u
G : SimpleGraph V
α : Type u_1
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : G.Coloring α
f : ⊤ ↪g G
⊢ s.card = card ↑↑s

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    bsup.{_, v} o f = blsub.{_, v} o f ∨ succ (bsup.{_, v} o f) = blsub.{_, v} o f

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ∨ succ (o.bsup f) = o.blsub f

Tactic:
rw [← sup_eq_bsup, ← lsub_eq_blsub]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ sup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ∨ succ (sup (o.familyOfBFamily f)) = lsub (o.familyOfBFamily f)

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ sup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ∨ succ (sup (o.familyOfBFamily f)) = lsub (o.familyOfBFamily f)

Tactic:
exact sup_eq_lsub_or_sup_succ_eq_lsub _

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma mul_delta_eq_smul_delta {f : ℕ → ℂ} : f * δ = f 1 • δ

Proof state:
case h
f : ℕ → ℂ
n : ℕ
⊢ (f * δ) n = (f 1 • δ) n

Tactic:
by_cases hn : n = 1 <;>
simp [hn, delta]

Result:
no goals

Proof state:
f : ℕ → ℂ
⊢ f * δ = f 1 • δ

Tactic:
ext n

Result:
case h
f : ℕ → ℂ
n : ℕ
⊢ (f * δ) n = (f 1 • δ) n
-- Mathlib/LinearAlgebra/Matrix/Symmetric.lean
theorem IsSymm.pow [CommSemiring α] [Fintype n] [DecidableEq n] {A : Matrix n n α} (h : A.IsSymm)
    (k : ℕ) :
    (A ^ k).IsSymm

Proof state:
α : Type u_1
n : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
⊢ (A ^ k).IsSymm

Tactic:
rw [IsSymm, transpose_pow, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
    as.all p start stop = !(as.any (!p ·) start stop)

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ as.all p start stop = !as.any (fun x => !p x) start stop

Tactic:
dsimp [all, allM]

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ (Id.run !anyM (fun v => !p v) as start stop) = !as.any (fun x => !p x) start stop

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ (Id.run !anyM (fun v => !p v) as start stop) = !as.any (fun x => !p x) start stop

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem isNoetherian_iff' : IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Tactic:
have := (CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this : WellFoundedGT (Submodule R M) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
⊢ IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this : WellFoundedGT (Submodule R M) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
⊢ IsNoetherian R M ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k

Tactic:
exact
  ⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h =>
    ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this : WellFoundedGT (Submodule R M) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
⊢ IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Tactic:
rw [this]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this : WellFoundedGT (Submodule R M) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
⊢ IsNoetherian R M ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_fst_le_log {b o : Ordinal.{u}} {x : Ordinal × Ordinal} :
    x ∈ CNF b o → x.1 ≤ log b o

Proof state:
case refine_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
rw [CNF_ne_zero ho, mem_cons]

Result:
case refine_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b o

Proof state:
case refine_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o

Tactic:
exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)

Result:
no goals

Proof state:
case refine_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b o

Tactic:
rintro (rfl | h)

Result:
case refine_2.inl
b o✝ o : Ordinal.{u}
ho : o ≠ 0
H : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).1 ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).1 ≤ log b o

case refine_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o

Proof state:
case refine_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.1 ≤ log b 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.inl
b o✝ o : Ordinal.{u}
ho : o ≠ 0
H : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).1 ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).1 ≤ log b o

Tactic:
rfl

Result:
no goals

Proof state:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
refine CNFRec b ?_ (fun o ho H ↦ ?_) o

Result:
case refine_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.1 ≤ log b 0

case refine_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.1 ≤ log b o
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem le_lfpApprox {a : Ordinal} : x ≤ lfpApprox f x a

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ≤ sSup ({x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x})

Tactic:
apply le_sSup

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ∈ {x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x}

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ≤ lfpApprox f x a

Tactic:
rw [lfpApprox]

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

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ∈ {x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x}

Tactic:
simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
theorem pullbackConeOfLeftIso_π_app_none : (pullbackConeOfLeftIso f g).π.app none = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app none = g

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.elim_countable_subcover_image {b : Set ι} {c : ι → Set X} (hs : IsLindelof s)
    (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) :
    ∃ b', b' ⊆ b ∧ Set.Countable b' ∧ s ⊆ ⋃ i ∈ b', c i

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ Subtype.val '' d ⊆ b

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
rcases hs.elim_countable_subcover (fun i ↦ c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩

Result:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Proof state:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ y ∈ d, c ↑y

Tactic:
exact hd.2

Result:
no goals

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ i ∈ b, IsOpen (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Proof state:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ i ∈ Subtype.val '' d, c i

Tactic:
rw [biUnion_image]

Result:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ y ∈ d, c ↑y

Proof state:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
refine ⟨Subtype.val '' d, by simp, Countable.image hd.1 Subtype.val, ?_⟩

Result:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ i ∈ Subtype.val '' d, c i
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem root {x : B} (hx : IsIntegral A x) {y : A} (h : IsRoot (minpoly A x) y) :
    algebraMap A B y = x

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : (Polynomial.aeval x) (minpoly A x) = 0
⊢ (algebraMap A B) y = x

Tactic:
rwa [key, map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
⊢ (algebraMap A B) y = x

Tactic:
have key : minpoly A x = X - C y := eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
  (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
    (dvd_iff_isRoot.2 h))

Result:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
⊢ (algebraMap A B) y = x

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
⊢ (algebraMap A B) y = x

Tactic:
have := aeval A x

Result:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : (Polynomial.aeval x) (minpoly A x) = 0
⊢ (algebraMap A B) y = x