harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma iterateFrobenius_mul_apply :
    iterateFrobenius R p (m * n) x = (iterateFrobenius R p m)^[n] x

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x

Tactic:
simp_rw [coe_iterateFrobenius, Function.iterate_mul]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem comp_assoc {a b c : V} :
    ∀ {d} (p : Path a b) (q : Path b c) (r : Path c d), (p.comp q).comp r = p.comp (q.comp r)
  | _, _, _, nil => rfl
  | _, p, q, cons r _ => by rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

Proof state:
V : Type u
inst✝ : Quiver V
a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ (p.comp q).comp (r.cons a✝) = p.comp (q.comp (r.cons a✝))

Tactic:
rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- The `k`-th shadow of a family of `r`-sets is a family of `r - k`-sets. -/
lemma _root_.Set.Sized.shadow_iterate (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    (∂^[k] 𝒜 : Set (Finset α)).Sized (r - k)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (∃ s ∈ 𝒜, x ⊆ s ∧ #(s \ x) = k) → #x = r - k

Tactic:
rintro t ⟨s, hs, hts, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ #t = r - #(s \ t)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ #t = r - #(s \ t)

Tactic:
rw [card_sdiff hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - k) ↑(∂ ^[k] 𝒜)

Tactic:
simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (∃ s ∈ 𝒜, x ⊆ s ∧ #(s \ x) = k) → #x = r - k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem some_eq_ite_none_right {p : Prop} [Decidable p] {b : Option α} :
    some a = (if p then b else none) ↔ p ∧ some a = b

Proof state:
α : Type u_1
a : α
p : Prop
inst✝ : Decidable p
b : Option α
⊢ (some a = if p then b else none) ↔ p ∧ some a = b

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem exists_nnreal_pos_mul_lt (ha : a ≠ ∞) (hb : b ≠ 0) : ∃ n > 0, ↑(n : ℝ≥0) * a < b

Proof state:
case intro.intro
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ ∃ n > 0, ↑n * a < b

Tactic:
use (n : ℝ≥0)⁻¹

Result:
case h
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ (↑n)⁻¹ > 0 ∧ ↑(↑n)⁻¹ * a < b

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
⊢ ∃ n > 0, ↑n * a < b

Tactic:
rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩

Result:
case intro.intro
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ ∃ n > 0, ↑n * a < b

Proof state:
case h
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ (↑n)⁻¹ > 0 ∧ ↑(↑n)⁻¹ * a < b

Tactic:
simp [*, npos.ne', zero_lt_one]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem iSup_induction' {ι : Sort*} (S : ι → Subalgebra R A) {motive : ∀ x, (x ∈ ⨆ i, S i) → Prop}
    {x : A} (mem : x ∈ ⨆ i, S i)
    (basic : ∀ (i) (x) (hx : x ∈ S i), motive x (mem_iSup_of_mem i hx))
    (zero : motive 0 (zero_mem _)) (one : motive 1 (one_mem _))
    (add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (add_mem ‹_› ‹_›))
    (mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem ‹_› ‹_›))
    (algebraMap : ∀ r, motive (algebraMap R A r) (Subalgebra.algebraMap_mem _ ‹_›)) :
    motive x mem

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
zero : motive 0 ⋯
one : motive 1 ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r) ⋯
⊢ ∃ (x_1 : x ∈ ⨆ i, S i), motive x x_1

Tactic:
exact iSup_induction S (motive := fun x' ↦ ∃ h, motive x' h) mem
  (fun _ _ h ↦ ⟨_, basic _ _ h⟩) ⟨_, zero⟩ ⟨_, one⟩ (fun _ _ h h' ↦ ⟨_, add _ _ _ _ h.2 h'.2⟩)
  (fun _ _ h h' ↦ ⟨_, mul _ _ _ _ h.2 h'.2⟩) fun _ ↦ ⟨_, algebraMap _⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
zero : motive 0 ⋯
one : motive 1 ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r) ⋯
⊢ motive x mem

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
zero : motive 0 ⋯
one : motive 1 ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r) ⋯
⊢ ∃ (x_1 : x ∈ ⨆ i, S i), motive x x_1
-- Mathlib/Topology/Basic.lean
theorem Set.Finite.isOpen_sInter {s : Set (Set X)} (hs : s.Finite) :
    (∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s) :=
  Finite.induction_on _ hs (fun _ => by rw [sInter_empty]; exact isOpen_univ) fun _ _ ih h => by
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
a✝ : Set X
s✝ : Set (Set X)
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen t) → IsOpen (⋂₀ s✝)
h : ∀ t ∈ insert a✝ s✝, IsOpen t
⊢ IsOpen (⋂₀ insert a✝ s✝)

Tactic:
simp only [sInter_insert, forall_mem_insert] at h ⊢

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
a✝ : Set X
s✝ : Set (Set X)
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen t) → IsOpen (⋂₀ s✝)
h : IsOpen a✝ ∧ ∀ x ∈ s✝, IsOpen x
⊢ IsOpen (a✝ ∩ ⋂₀ s✝)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
a✝ : Set X
s✝ : Set (Set X)
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen t) → IsOpen (⋂₀ s✝)
h : IsOpen a✝ ∧ ∀ x ∈ s✝, IsOpen x
⊢ IsOpen (a✝ ∩ ⋂₀ s✝)

Tactic:
exact h.1.inter (ih h.2)

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
x✝ : ∀ t ∈ ∅, IsOpen t
⊢ IsOpen (⋂₀ ∅)

Tactic:
rw [sInter_empty]

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
x✝ : ∀ t ∈ ∅, IsOpen t
⊢ IsOpen univ

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
x✝ : ∀ t ∈ ∅, IsOpen t
⊢ IsOpen univ

Tactic:
exact isOpen_univ

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem toMeasure_pure : (pure a).toMeasure = Measure.dirac a :=
  Measure.ext fun s hs => by rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]; rfl

Proof state:
α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (pure a).toMeasure s = (Measure.dirac a) s

Tactic:
rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]

Result:
α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = s.indicator 1 a

Proof state:
α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = s.indicator 1 a

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Sigma.map'_comp_map' {f : α → C} {g : β → C} {h : γ → C} [HasCoproduct f] [HasCoproduct g]
    [HasCoproduct h] (p : α → β) (p' : β → γ) (q : ∀ (a : α), f a ⟶ g (p a))
    (q' : ∀ (b : β), g b ⟶ h (p' b)) :
    Sigma.map' p q ≫ Sigma.map' p' q' = Sigma.map' (p' ∘ p) (fun a => q a ≫ q' (p a))

Proof state:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
⊢ map' p q ≫ map' p' q' = map' (p' ∘ p) fun a => q a ≫ q' (p a)

Tactic:
ext

Result:
case h
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map' p' q' = ι f b✝ ≫ map' (p' ∘ p) fun a => q a ≫ q' (p a)

Proof state:
case h
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map' p' q' = ι f b✝ ≫ map' (p' ∘ p) fun a => q a ≫ q' (p a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_toArray {α n} (xs : Vector α n) (i : Nat) :
    xs.toArray[i]? = xs[i]?

Proof state:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray[i]? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
i : Nat
⊢ xs.toArray[i]? = xs[i]?

Tactic:
cases xs

Result:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray[i]? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
    [Countable ι] [Preorder ι] {f : ι → Set α} (hm : ∀ i, NullMeasurableSet (f i) μ)
    (hf : ∃ i, μ (f i) ≠ ∞) :
    Tendsto (fun i ↦ μ (⋂ j ≤ i, f j)) atTop (𝓝 (μ (⋂ i, f i)))

Proof state:
case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
rw [measure_iInter_eq_iInf_measure_iInter_le hm hf]

Result:
case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)))

Proof state:
case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)))

Tactic:
exact tendsto_atTop_iInf
  fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij

Result:
no goals

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
refine .of_neBot_imp fun hne ↦ ?_

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
hne : atTop.NeBot
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
hne : atTop.NeBot
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
cases atTop_neBot_iff.mp hne

Result:
case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ⊤
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem one_le_rpow {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (hz : 0 < z) : 1 ≤ x ^ z

Proof state:
case top
z : ℝ
hz : 0 < z
hx : 1 ≤ ⊤
⊢ 1 ≤ ⊤ ^ z

Tactic:
simp [top_rpow_of_pos hz]

Result:
no goals

Proof state:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ 1 ≤ ↑x✝ ^ z

Tactic:
simp only [one_le_coe_iff, some_eq_coe] at hx

Result:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 ≤ x✝
⊢ 1 ≤ ↑x✝ ^ z

Proof state:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 ≤ x✝
⊢ 1 ≤ ↑x✝ ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_le_rpow hx (le_of_lt hz)]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
⊢ 1 ≤ x ^ z

Tactic:
cases x

Result:
case top
z : ℝ
hz : 0 < z
hx : 1 ≤ ⊤
⊢ 1 ≤ ⊤ ^ z

case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ 1 ≤ ↑x✝ ^ z
-- Mathlib/RingTheory/Nilpotent/Defs.lean
lemma isNilpotent_of_pos_nilpotencyClass (hx : 0 < nilpotencyClass x) :
    IsNilpotent x

Proof state:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k | x ^ k = 0}
⊢ IsNilpotent x

Tactic:
change s.Nonempty

Result:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k | x ^ k = 0}
⊢ s.Nonempty

Proof state:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
s : Set ℕ := {k | x ^ k = 0}
hx : 0 < sInf s
⊢ s.Nonempty

Tactic:
by_contra contra

Result:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
s : Set ℕ := {k | x ^ k = 0}
hx : 0 < sInf s
contra : ¬s.Nonempty
⊢ False

Proof state:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
⊢ IsNilpotent x

Tactic:
let s : Set ℕ := {k | x ^ k = 0}

Result:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k | x ^ k = 0}
⊢ IsNilpotent x

Proof state:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
s : Set ℕ := {k | x ^ k = 0}
hx : 0 < sInf s
contra : ¬s.Nonempty
⊢ False

Tactic:
simp [not_nonempty_iff_eq_empty.mp contra] at hx

Result:
no goals

Proof state:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k | x ^ k = 0}
⊢ s.Nonempty

Tactic:
change 0 < sInf s at hx

Result:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
s : Set ℕ := {k | x ^ k = 0}
hx : 0 < sInf s
⊢ s.Nonempty
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem ker_liftQ_eq_bot (f : M →ₛₗ[τ₁₂] M₂) (h) (h' : ker f ≤ p) : ker (p.liftQ f h) = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
h' : ker f ≤ p
⊢ ker (p.liftQ f h) = ⊥

Tactic:
rw [ker_liftQ, le_antisymm h h', mkQ_map_self]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_lt_smul_iff_of_neg_left (ha : a < 0) : a • b₁ < a • b₂ ↔ b₂ < b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ -a • b₂ < -a • b₁ ↔ b₂ < b₁

Tactic:
exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg ha)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b₁ < a • b₂ ↔ b₂ < b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]

Result:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ -a • b₂ < -a • b₁ ↔ b₂ < b₁
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma bot_preconnected_iff_subsingleton : (⊥ : SimpleGraph V).Preconnected ↔ Subsingleton V

Proof state:
V : Type u
h : ⊥.Preconnected
⊢ Subsingleton V

Tactic:
contrapose h

Result:
V : Type u
h : ¬Subsingleton V
⊢ ¬⊥.Preconnected

Proof state:
V : Type u
h : Subsingleton V
⊢ ⊥.Preconnected

Tactic:
simpa [subsingleton_iff, ← reachable_bot] using h

Result:
no goals

Proof state:
V : Type u
h : ¬Subsingleton V
⊢ ¬⊥.Preconnected

Tactic:
simp [nontrivial_iff.mp <| not_subsingleton_iff_nontrivial.mp h, Preconnected, reachable_bot, h]

Result:
no goals

Proof state:
V : Type u
⊢ ⊥.Preconnected ↔ Subsingleton V

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simpa [subsingleton_iff, ← reachable_bot] using h⟩

Result:
V : Type u
h : ⊥.Preconnected
⊢ Subsingleton V
-- Mathlib/RingTheory/LaurentSeries.lean
theorem mem_integers_of_powerSeries (F : K⟦X⟧) :
    (LaurentSeriesRingEquiv K) F ∈ (idealX K).adicCompletionIntegers (RatFunc K)

Proof state:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ ∃ F_1, (ofPowerSeries ℤ K) F_1 = (ofPowerSeries ℤ K) F

Tactic:
exact ⟨F, rfl⟩

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Tactic:
simp only [Subring.mem_map, exists_prop, ValuationSubring.mem_toSubring,
  mem_adicCompletionIntegers, LaurentSeriesRingEquiv_def,
  valuation_compare, val_le_one_iff_eq_coe]

Result:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ ∃ F_1, (ofPowerSeries ℤ K) F_1 = (ofPowerSeries ℤ K) F
-- Mathlib/Combinatorics/Colex.lean
lemma geomSum_ofColex_strictMono (hn : 2 ≤ n) : StrictMono fun s ↦ ∑ k ∈ ofColex s, n ^ k

Proof state:
case toColex.toColex
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
hst : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }

Tactic:
obtain ⟨a, hat, has, ha⟩ := hst

Result:
case toColex.toColex.intro.intro.intro
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
a : ℕ
hat : a ∈ t
has : a ∉ s
ha : ∀ b ∈ s, b ∉ t → b < a
⊢ (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }

Proof state:
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
a : ℕ
hat : a ∈ t
has : a ∉ s
ha : ∀ b ∈ s, b ∉ t → b < a
⊢ ∀ k ∈ { ofColex := s }.ofColex \ { ofColex := t }.ofColex, k < a

Tactic:
simpa

Result:
no goals

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ StrictMono fun s => ∑ k ∈ s.ofColex, n ^ k

Tactic:
rintro ⟨s⟩ ⟨t⟩ hst

Result:
case toColex.toColex
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
hst : { ofColex := s } < { ofColex := t }
⊢ (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }

Proof state:
case toColex.toColex
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
hst : { ofColex := s } < { ofColex := t }
⊢ (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }

Tactic:
rw [toColex_lt_toColex_iff_exists_forall_lt] at hst

Result:
case toColex.toColex
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
hst : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }

Proof state:
case toColex.toColex.intro.intro.intro
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
a : ℕ
hat : a ∈ t
has : a ∉ s
ha : ∀ b ∈ s, b ∉ t → b < a
⊢ ∑ i ∈ { ofColex := s }.ofColex \ { ofColex := t }.ofColex, n ^ i <
    ∑ i ∈ { ofColex := t }.ofColex \ { ofColex := s }.ofColex, n ^ i

Tactic:
exact (Nat.geomSum_lt hn <| by simpa).trans_le <| single_le_sum (fun _ _ ↦ by positivity) <|
  mem_sdiff.2 ⟨hat, has⟩

Result:
no goals

Proof state:
case toColex.toColex.intro.intro.intro
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
a : ℕ
hat : a ∈ t
has : a ∉ s
ha : ∀ b ∈ s, b ∉ t → b < a
⊢ (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }

Tactic:
rw [← sum_sdiff_lt_sum_sdiff]

Result:
case toColex.toColex.intro.intro.intro
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
a : ℕ
hat : a ∈ t
has : a ∉ s
ha : ∀ b ∈ s, b ∉ t → b < a
⊢ ∑ i ∈ { ofColex := s }.ofColex \ { ofColex := t }.ofColex, n ^ i <
    ∑ i ∈ { ofColex := t }.ofColex \ { ofColex := s }.ofColex, n ^ i

Proof state:
n : ℕ
hn : 2 ≤ n
s t : Finset ℕ
a : ℕ
hat : a ∈ t
has : a ∉ s
ha : ∀ b ∈ s, b ∉ t → b < a
x✝¹ : ℕ
x✝ : x✝¹ ∈ { ofColex := t }.ofColex \ { ofColex := s }.ofColex
⊢ 0 ≤ n ^ x✝¹

Tactic:
positivity

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_ord_mem_fixedPoint (h_init : x ≤ f x) :
    lfpApprox f x (ord <| succ #α) ∈ fixedPoints f

Proof state:
case inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_init : x ≤ f x
a : Ordinal.{u}
h_a : a < (succ #α).ord
b : Ordinal.{u}
h_b : b < (succ #α).ord
h_nab : a ≠ b
h_fab : lfpApprox f x a = lfpApprox f x b
h_ba : b ≤ a
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
exact lfpApprox_mem_fixedPoints_of_eq f x h_init
  (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_init : x ≤ f x
a : Ordinal.{u}
h_a : a < (succ #α).ord
b : Ordinal.{u}
h_b : b < (succ #α).ord
h_nab : a ≠ b
h_fab : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
cases le_total a b with
| inl h_ab =>
  exact lfpApprox_mem_fixedPoints_of_eq f x h_init
    (h_nab.lt_of_le h_ab) (le_of_lt h_a) h_fab
| inr h_ba =>
  exact lfpApprox_mem_fixedPoints_of_eq f x h_init
    (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)

Result:
no goals

Proof state:
case inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_init : x ≤ f x
a : Ordinal.{u}
h_a : a < (succ #α).ord
b : Ordinal.{u}
h_b : b < (succ #α).ord
h_nab : a ≠ b
h_fab : lfpApprox f x a = lfpApprox f x b
h_ab : a ≤ b
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
exact lfpApprox_mem_fixedPoints_of_eq f x h_init
  (h_nab.lt_of_le h_ab) (le_of_lt h_a) h_fab

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_init : x ≤ f x
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := exists_lfpApprox_eq_lfpApprox f x

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_init : x ≤ f x
a : Ordinal.{u}
h_a : a < (succ #α).ord
b : Ordinal.{u}
h_b : b < (succ #α).ord
h_nab : a ≠ b
h_fab : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma mapSpanningSubgraphs_inj {G G' : SimpleGraph V} {v w : V} (h : G ≤ G') :
    mapSpanningSubgraphs h v = mapSpanningSubgraphs h w ↔ v = w

Proof state:
V : Type u_1
G G' : SimpleGraph V
v w : V
h : G ≤ G'
⊢ (mapSpanningSubgraphs h) v = (mapSpanningSubgraphs h) w ↔ v = w

Tactic:
simp

Result:
no goals