harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Support.lean
theorem disjoint_iff_disjoint_support : Disjoint f g ↔ _root_.Disjoint f.support g.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f.Disjoint g ↔ _root_.Disjoint f.support g.support

Tactic:
simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff, not_and_or,
  imp_iff_not_or]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem gosper_catalan_sub_eq_central_binom_div (n : ℕ) : gosperCatalan (n + 1) (n + 1) -
    gosperCatalan (n + 1) 0 = Nat.centralBinom (n + 1) / (n + 2)

Proof state:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ ↑n + 2 ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ (↑(n + 1).centralBinom * (2 * (↑n + 1) - (↑n + 1)) - ↑(n + 1).centralBinom * (-1 + -↑n)) * (↑n + 2) =
    ↑(n + 1).centralBinom * (2 * (↑n + 1) * (↑n + 1 + 1))

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
simp only [gosperCatalan, Nat.sub_zero, Nat.centralBinom_zero, Nat.sub_self]

Result:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ ↑(n + 1).centralBinom * ↑1 * (2 * ↑(n + 1) - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑1 * ↑(n + 1).centralBinom * (2 * ↑0 - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(n + 1).centralBinom / (↑n + 2)

Proof state:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ ↑(n + 1).centralBinom * ↑1 * (2 * ↑(n + 1) - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑1 * ↑(n + 1).centralBinom * (2 * ↑0 - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
field_simp

Result:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ (↑(n + 1).centralBinom * (2 * (↑n + 1) - (↑n + 1)) - ↑(n + 1).centralBinom * (-1 + -↑n)) * (↑n + 2) =
    ↑(n + 1).centralBinom * (2 * (↑n + 1) * (↑n + 1 + 1))

Proof state:
n : ℕ
this : ↑n + 1 ≠ 0
⊢ ↑n + 1 + 1 ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
have h : (n : ℚ) + 2 ≠ 0 := by norm_cast

Result:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Proof state:
n : ℕ
this : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
have : (n : ℚ) + 1 + 1 ≠ 0 := by norm_cast

Result:
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Proof state:
n : ℕ
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
have : (n : ℚ) + 1 ≠ 0 := by norm_cast

Result:
n : ℕ
this : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Proof state:
n : ℕ
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_mul' (h : leadingCoeff p * leadingCoeff q ≠ 0) :
    leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
unfold leadingCoeff

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).coeff (p * q).natDegree = p.coeff p.natDegree * q.coeff q.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = p.coeff p.natDegree * q.coeff q.natDegree

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).coeff (p * q).natDegree = p.coeff p.natDegree * q.coeff q.natDegree

Tactic:
rw [natDegree_mul' h, coeff_mul_degree_add_degree]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = p.coeff p.natDegree * q.coeff q.natDegree
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem comp {g : β → γ} {f : α → β} (hg : MeasurePreserving g μb μc)
    (hf : MeasurePreserving f μa μb) : MeasurePreserving (g ∘ f) μa μc :=
  ⟨hg.1.comp hf.1, by rw [← map_map hg.1 hf.1, hf.2, hg.2]⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : MeasurePreserving g μb μc
hf : MeasurePreserving f μa μb
⊢ map (g ∘ f) μa = μc

Tactic:
rw [← map_map hg.1 hf.1, hf.2, hg.2]

Result:
no goals
-- Mathlib/Data/Sym/Card.lean
lemma two_mul_card_image_offDiag (s : Finset α) : 2 * #(s.offDiag.image Sym2.mk) = #s.offDiag

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
have : {z ∈ s.offDiag | Sym2.mk z = s(x, y)} = {(x, y), (y, x)} := by
  ext ⟨x₁, y₁⟩
  rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff,
    and_iff_right_iff_imp]
  rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2
-- Mathlib/Data/Setoid/Partition.lean
lemma _root_.Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty {α : Type*} {s : Set (Set α)}
    (h₁ : s.PairwiseDisjoint id) (h₂ : ∀ a : α, ∃ x ∈ s, a ∈ x) (h₃ : ∅ ∉ s) :
    Setoid.IsPartition s

Proof state:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ b₁ = b₂

Tactic:
apply h₁.elim hb₁.1 hb₂.1

Result:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ¬Disjoint (id b₁) (id b₂)

Proof state:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ∃ x ∈ id b₁, x ∈ id b₂

Tactic:
exact ⟨a, hb₁.2, hb₂.2⟩

Result:
no goals

Proof state:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
⊢ IsPartition s

Tactic:
refine ⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩

Result:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
⊢ ∀ (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂

Proof state:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
⊢ ∀ (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂

Tactic:
intro b₁ b₂ hb₁ hb₂

Result:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ b₁ = b₂

Proof state:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ¬Disjoint (id b₁) (id b₂)

Tactic:
simp only [Set.not_disjoint_iff]

Result:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ∃ x ∈ id b₁, x ∈ id b₂
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem UniformSpace.comap_iInf {ι α γ} {u : ι → UniformSpace γ} {f : α → γ} :
    (⨅ i, u i).comap f = ⨅ i, (u i).comap f

Proof state:
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ i, u i) = ⨅ i, comap f (u i)

Tactic:
ext : 1

Result:
case h
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ 𝓤 α = 𝓤 α

Proof state:
case h
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ 𝓤 α = 𝓤 α

Tactic:
simp [uniformity_comap, iInf_uniformity]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_succ (o) : cof (succ o) = 1

Proof state:
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ ↑1 = 1

Tactic:
simp

Result:
no goals

Proof state:
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ #↑{Sum.inr PUnit.unit} = 1

Tactic:
rw [Cardinal.mk_fintype, Set.card_singleton]

Result:
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ ↑1 = 1

Proof state:
case a
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (type (Sum.Lex r EmptyRelation)).cof ≤ 1

Tactic:
rw [← (_ : #_ = 1)]

Result:
case a
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (type (Sum.Lex r EmptyRelation)).cof ≤ #?m.45778

o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ #?m.45778 = 1

Proof state:
case a
o : Ordinal.{u_1}
⊢ 1 ≤ (succ o).cof

Tactic:
rw [← Cardinal.succ_zero, succ_le_iff]

Result:
case a
o : Ordinal.{u_1}
⊢ 0 < (succ o).cof

Proof state:
case a.h
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Unbounded (Sum.Lex r EmptyRelation) ?a.S✝

case a.S
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Set (α ⊕ PUnit.{u_1 + 1})

Tactic:
refine fun a => ⟨Sum.inr PUnit.unit, Set.mem_singleton _, ?_⟩

Result:
case a.h
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
a : α ⊕ PUnit.{u_1 + 1}
⊢ ¬Sum.Lex r EmptyRelation (Sum.inr PUnit.unit) a

Proof state:
case a
o : Ordinal.{u_1}
⊢ (succ o).cof ≤ 1

Tactic:
refine inductionOn o fun α r _ => ?_

Result:
case a
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (succ (type r)).cof ≤ 1

Proof state:
case a.h
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
a : α ⊕ PUnit.{u_1 + 1}
⊢ ¬Sum.Lex r EmptyRelation (Sum.inr PUnit.unit) a

Tactic:
rcases a with (a | ⟨⟨⟨⟩⟩⟩) <;> simp [EmptyRelation]

Result:
no goals

Proof state:
case a
o : Ordinal.{u_1}
⊢ 0 < (succ o).cof

Tactic:
simpa [lt_iff_le_and_ne, Cardinal.zero_le] using fun h =>
  succ_ne_zero o (cof_eq_zero.1 (Eq.symm h))

Result:
no goals

Proof state:
case a
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (type (Sum.Lex r EmptyRelation)).cof ≤ #?m.45778

Tactic:
apply cof_type_le

Result:
case a.h
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Unbounded (Sum.Lex r EmptyRelation) ?a.S✝

case a.S
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Set (α ⊕ PUnit.{u_1 + 1})

Proof state:
o : Ordinal.{u_1}
⊢ (succ o).cof = 1

Tactic:
apply le_antisymm

Result:
case a
o : Ordinal.{u_1}
⊢ (succ o).cof ≤ 1

case a
o : Ordinal.{u_1}
⊢ 1 ≤ (succ o).cof

Proof state:
case a
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (succ (type r)).cof ≤ 1

Tactic:
change cof (type _) ≤ _

Result:
case a
o : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (type (Sum.Lex r EmptyRelation)).cof ≤ 1
-- Mathlib/Data/Set/Function.lean
theorem injOn_image (h : Semiconj f fa fb) (ha : InjOn fa s) (hf : InjOn f (fa '' s)) :
    InjOn fb (f '' s)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y

Tactic:
simp only [← h.eq] at H

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y

Tactic:
exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
⊢ InjOn fb (f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ H

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α → Prop)
    (hadm : admissible P) : admissible (fun (x : α ×' β) => P x.1)

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.fst) x
⊢ P (CCPO.csup c).fst

Tactic:
apply hadm _ (PProd.chain.chain_fst hchain)

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.fst) x
⊢ ∀ (x : α), PProd.chain.fst c x → P x

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.fst) x
x : α
y : β
hxy : c ⟨x, y⟩
⊢ P x

Tactic:
apply h ⟨x,y⟩ hxy

Result:
no goals

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.fst) x
⊢ ∀ (x : α), PProd.chain.fst c x → P x

Tactic:
intro x ⟨y, hxy⟩

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.fst) x
x : α
y : β
hxy : c ⟨x, y⟩
⊢ P x

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
⊢ admissible fun x => P x.fst

Tactic:
intro c hchain h

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : α → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.fst) x
⊢ P (CCPO.csup c).fst
-- Mathlib/RingTheory/DualNumber.lean
lemma ideal_trichotomy [DivisionRing K] (I : Ideal K[ε]) :
    I = ⊥ ∨ I = .span {ε} ∨ I = ⊤

Proof state:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ ∃ r_1, ε = r_1 * (ε * r)

Tactic:
have : ε * r = (fst r) • ε := by ext <;> simp

Result:
case intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
this : ε * r = fst r • ε
⊢ ∃ r_1, ε = r_1 * (ε * r)

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ I = Ideal.span {ε}

Tactic:
have hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x := by
  intro x hxI hx0
  obtain ⟨r, rfl⟩ := hd _ hxI
  have : ε * r = (fst r) • ε := by ext <;> simp
  rw [this] at hxI hx0 ⊢
  have hr : fst r ≠ 0 := by
    contrapose! hx0
    simp [hx0]
  refine ⟨r⁻¹, ?_⟩
  simp [TrivSqZeroExt.ext_iff, inv_mul_cancel₀ hr]

Result:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
⊢ I = Ideal.span {ε}

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
hx0 : fst r • ε ≠ 0
this : ε * r = fst r • ε
⊢ fst r ≠ 0

Tactic:
contrapose! hx0

Result:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : fst r • ε ∈ I
this : ε * r = fst r • ε
hx0 : fst r = 0
⊢ fst r • ε = 0

Proof state:
case refine_2.intro.intro.intro.intro
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ p * r * y ∈ I

Tactic:
exact Ideal.mul_mem_left _ _ hyI

Result:
no goals

Proof state:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
⊢ ε ∣ x

Tactic:
rcases isUnit_or_isNilpotent x with hx|hx

Result:
case inl
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsUnit x
⊢ ε ∣ x

case inr
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsNilpotent x
⊢ ε ∣ x
-- Mathlib/Data/Sign.lean
theorem univ_eq : (Finset.univ : Finset SignType) = {0, -1, 1}

Proof state:
⊢ Finset.univ = {0, -1, 1}

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Analysis/Topology.lean
theorem ofEquiv_F (F : Realizer α) (E : F.σ ≃ τ) (s : τ) : (F.ofEquiv E).F s = F.F (E.symm s)

Proof state:
α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }.F.f s = F.F.f (E.symm s)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ (F.ofEquiv E).F.f s = F.F.f (E.symm s)

Tactic:
delta ofEquiv

Result:
α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }.F.f s = F.F.f (E.symm s)
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem nonpos_of_restrict_le_zero (hi₂ : v ≤[i] 0) : v i ≤ 0

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : ¬MeasurableSet i
⊢ ↑v i ≤ 0

Tactic:
rw [v.not_measurable hi₁]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : MeasurableSet i
⊢ ↑v i ≤ 0

Tactic:
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
⊢ ↑v i ≤ 0

Tactic:
by_cases hi₁ : MeasurableSet i

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : MeasurableSet i
⊢ ↑v i ≤ 0

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : ¬MeasurableSet i
⊢ ↑v i ≤ 0
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem dist_t₀_le (t : Icc v.tMin v.tMax) : dist t v.t₀ ≤ v.tDist

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ |↑t - ↑v.t₀| ≤ v.tDist

Tactic:
rw [abs_of_nonneg (sub_nonneg.2 <| Subtype.coe_le_coe.2 ht)]

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ ↑t - ↑v.t₀ ≤ v.tDist

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ ↑t - ↑v.t₀ ≤ v.tDist

Tactic:
exact (sub_le_sub_right t.2.2 _).trans (le_max_left _ _)

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ |↑t - ↑v.t₀| ≤ v.tDist

Tactic:
rw [abs_of_nonpos (sub_nonpos.2 <| Subtype.coe_le_coe.2 ht), neg_sub]

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ ↑v.t₀ - ↑t ≤ v.tDist

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ |↑t - ↑v.t₀| ≤ v.tDist

Tactic:
rcases le_total t v.t₀ with ht | ht

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ |↑t - ↑v.t₀| ≤ v.tDist

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ |↑t - ↑v.t₀| ≤ v.tDist

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ dist t v.t₀ ≤ v.tDist

Tactic:
rw [Subtype.dist_eq, Real.dist_eq]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ |↑t - ↑v.t₀| ≤ v.tDist

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ ↑v.t₀ - ↑t ≤ v.tDist

Tactic:
exact (sub_le_sub_left t.2.1 _).trans (le_max_right _ _)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_nsmul (m : Multiset α) : ∀ n : ℕ, (n • m).prod = m.prod ^ n
  | 0 => by
    rw [zero_nsmul, pow_zero]
    rfl
  | n + 1 => by rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]

Proof state:
α : Type u_3
inst✝ : CommMonoid α
m : Multiset α
n : ℕ
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)

Tactic:
rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
m : Multiset α
⊢ prod 0 = 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
m : Multiset α
⊢ (0 • m).prod = m.prod ^ 0

Tactic:
rw [zero_nsmul, pow_zero]

Result:
α : Type u_3
inst✝ : CommMonoid α
m : Multiset α
⊢ prod 0 = 1
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_sub (a b c : Ordinal) : a * (b - c) = a * b - a * c :=
  if a0 : a = 0 then by simp only [a0, zero_mul, sub_self]
  else
    eq_of_forall_ge_iff fun d => by rw [sub_le, ← le_div a0, sub_le, ← le_div a0, mul_add_div _ a0]

Proof state:
a b c : Ordinal.{u_4}
a0 : a = 0
⊢ a * (b - c) = a * b - a * c

Tactic:
simp only [a0, zero_mul, sub_self]

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
a0 : ¬a = 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d

Tactic:
rw [sub_le, ← le_div a0, sub_le, ← le_div a0, mul_add_div _ a0]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma div_conj_eq_sub_one : p / q = p - 1

Proof state:
case inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hq : q ≠ ⊤
⊢ p / q + 1 = p

Tactic:
rw [← ENNReal.div_self h.symm.ne_zero hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
  ENNReal.div_self h.symm.ne_zero hq, mul_one]

Result:
no goals

Proof state:
case inl
p : ℝ≥0∞
h : p.IsConjExponent ⊤
⊢ p / ⊤ = p - 1

Tactic:
simp [h.symm.conj_eq, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ p / q = p - 1

Tactic:
obtain rfl | hq := eq_or_ne q ∞

Result:
case inl
p : ℝ≥0∞
h : p.IsConjExponent ⊤
⊢ p / ⊤ = p - 1

case inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hq : q ≠ ⊤
⊢ p / q = p - 1

Proof state:
case inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hq : q ≠ ⊤
⊢ p / q = p - 1

Tactic:
refine ENNReal.eq_sub_of_add_eq one_ne_top ?_

Result:
case inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hq : q ≠ ⊤
⊢ p / q + 1 = p