harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
lemma spine_map_subinterval {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (Δ : X _⦋n⦌) :
    X.spine l (X.map (subinterval j l (by omega)).op Δ) =
      (X.spine n Δ).interval j l (by omega)

Proof state:
case arrow.h
X : SSet
n j l : ℕ
hjl : j + l ≤ n
Δ : X _⦋n⦌
i : Fin l
⊢ (X.spine l (X.map (subinterval j l ⋯).op Δ)).arrow i = ((X.spine n Δ).interval j l ⋯).arrow i

Tactic:
simp only [spine_arrow, Path.interval, ← FunctorToTypes.map_comp_apply, ← op_comp,
  mkOfSucc_subinterval_eq]

Result:
no goals

Proof state:
case vertex.h
X : SSet
n j l : ℕ
hjl : j + l ≤ n
Δ : X _⦋n⦌
i : Fin (l + 1)
⊢ (X.spine l (X.map (subinterval j l ⋯).op Δ)).vertex i = ((X.spine n Δ).interval j l ⋯).vertex i

Tactic:
simp only [spine_vertex, Path.interval, ← FunctorToTypes.map_comp_apply, ← op_comp,
  const_subinterval_eq]

Result:
no goals

Proof state:
X : SSet
n j l : ℕ
hjl : j + l ≤ n
Δ : X _⦋n⦌
⊢ j + l ≤ n

Tactic:
omega

Result:
no goals

Proof state:
X : SSet
n j l : ℕ
hjl : j + l ≤ n
Δ : X _⦋n⦌
⊢ X.spine l (X.map (subinterval j l ⋯).op Δ) = (X.spine n Δ).interval j l ⋯

Tactic:
ext i

Result:
case vertex.h
X : SSet
n j l : ℕ
hjl : j + l ≤ n
Δ : X _⦋n⦌
i : Fin (l + 1)
⊢ (X.spine l (X.map (subinterval j l ⋯).op Δ)).vertex i = ((X.spine n Δ).interval j l ⋯).vertex i

case arrow.h
X : SSet
n j l : ℕ
hjl : j + l ≤ n
Δ : X _⦋n⦌
i : Fin l
⊢ (X.spine l (X.map (subinterval j l ⋯).op Δ)).arrow i = ((X.spine n Δ).interval j l ⋯).arrow i
-- Mathlib/Analysis/Convex/Exposed.lean
theorem isExtreme (hAB : IsExposed 𝕜 A B) : IsExtreme 𝕜 A B

Proof state:
case intro.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hl : ConvexOn 𝕜 univ ⇑l
hlx₁ : l x₁ ≤ l x
hlx₂ : l x₂ ≤ l x
y : E
hy : y ∈ A
⊢ l y ≤ l x

Tactic:
exact hxB.2 y hy

Result:
no goals

Proof state:
case intro.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hl : ConvexOn 𝕜 univ ⇑l
hlx₁ : l x₁ ≤ l x
hlx₂ : l x₂ ≤ l x
y : E
hy : y ∈ A
⊢ l y ≤ l x₂

Tactic:
rw [hlx₂.antisymm (hl.le_right_of_left_le (mem_univ _) (mem_univ _) hx hlx₁)]

Result:
case intro.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hl : ConvexOn 𝕜 univ ⇑l
hlx₁ : l x₁ ≤ l x
hlx₂ : l x₂ ≤ l x
y : E
hy : y ∈ A
⊢ l y ≤ l x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem mul_resolve_left_inv_le (a p k : Int) (a_pos : 0 < a)
    (h₃ : b * k + b * p ≤ a * q) (h₄ : a ∣ k + p) :
    b * resolve_left_inv a p k ≤ q

Proof state:
b q a p k : Int
a_pos : 0 < a
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
⊢ b * resolve_left_inv a p k ≤ q

Tactic:
suffices h : a * (b * ((k + p) / a)) ≤ a * q from le_of_mul_le_mul_left h a_pos

Result:
b q a p k : Int
a_pos : 0 < a
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
⊢ a * (b * ((k + p) / a)) ≤ a * q

Proof state:
b q a p k : Int
a_pos : 0 < a
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
⊢ a * (b * ((k + p) / a)) ≤ a * q

Tactic:
rw [Int.mul_left_comm a b, Int.mul_ediv_cancel' h₄, Int.mul_add]

Result:
b q a p k : Int
a_pos : 0 < a
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
⊢ b * k + b * p ≤ a * q

Proof state:
b q a p k : Int
a_pos : 0 < a
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
⊢ b * k + b * p ≤ a * q

Tactic:
exact h₃

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber (hι : s.WellFoundedOn (rι on f))
    (hπ : ∀ i, (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)) :
    s.WellFoundedOn (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)

Proof state:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ WellFounded (Sigma.Lex rι rπ on fun c => ⟨f ↑c, g (f ↑c) ↑c⟩)

Tactic:
exact
  @WellFounded.sigma_lex_of_wellFoundedOn_fiber _ s _ _ rπ (fun c => f c) (fun i c => g _ c) hι
    fun i => ((hπ i).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun b c h => ‹_›)

Result:
no goals

Proof state:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ s.WellFoundedOn (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)

Tactic:
show WellFounded (Sigma.Lex rι rπ on fun c : s => ⟨f c, g (f c) c⟩)

Result:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ WellFounded (Sigma.Lex rι rπ on fun c => ⟨f ↑c, g (f ↑c) ↑c⟩)
-- Mathlib/Order/Filter/Map.lean
theorem map_le_map_iff {f g : Filter α} {m : α → β} (hm : Injective m) :
    map m f ≤ map m g ↔ f ≤ g

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ map m f ≤ map m g ↔ f ≤ g

Tactic:
rw [map_le_iff_le_comap, comap_map hm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Subperm.cons_left {l₁ l₂ : List α} (h : l₁ <+~ l₂) (x : α) (hx : count x l₁ < count x l₂) :
    x :: l₁ <+~ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ y ∈ l₁

Tactic:
simpa [hy'] using hy

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y (x :: l₁) ≤ count y l₂

Tactic:
rw [count_cons_of_ne hy']

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y l₁ ≤ count y l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
⊢ count y (x :: l₁) ≤ count y l₂

Tactic:
if hy' : y = x then
  subst x; simpa using Nat.succ_le_of_lt hx
else
  rw [count_cons_of_ne hy']
  refine h y ?_
  simpa [hy'] using hy

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
⊢ ∀ (x_1 : α), x_1 ∈ x :: l₁ → count x_1 (x :: l₁) ≤ count x_1 l₂

Tactic:
intro y hy

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
⊢ count y (x :: l₁) ≤ count y l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y l₁ ≤ count y l₂

Tactic:
refine h y ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ y ∈ l₁

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <+~ l₂
x : α
hx : count x l₁ < count x l₂
⊢ x :: l₁ <+~ l₂

Tactic:
rw [subperm_ext_iff] at h ⊢

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
⊢ ∀ (x_1 : α), x_1 ∈ x :: l₁ → count x_1 (x :: l₁) ≤ count x_1 l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : y = x
⊢ count y (x :: l₁) ≤ count y l₂

Tactic:
subst x

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
y : α
hx : count y l₁ < count y l₂
hy : y ∈ y :: l₁
⊢ count y (y :: l₁) ≤ count y l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
y : α
hx : count y l₁ < count y l₂
hy : y ∈ y :: l₁
⊢ count y (y :: l₁) ≤ count y l₂

Tactic:
simpa using Nat.succ_le_of_lt hx

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_le_smul_of_nonpos_left (h : b₁ ≤ b₂) (ha : a ≤ 0) : a • b₂ ≤ a • b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ -a • b₁ ≤ -a • b₂

Tactic:
exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ a • b₂ ≤ a • b₁

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

Result:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ -a • b₁ ≤ -a • b₂
-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem _root_.FiniteField.isSplittingField_of_nat_card_eq (h : Nat.card K = p ^ n) :
    IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Tactic:
rw [← h, Nat.card_eq_fintype_card]

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ Fintype.card K - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ Fintype.card K - X)

Tactic:
exact FiniteField.isSplittingField_sub K (ZMod p)

Result:
no goals

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this : Finite K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Tactic:
haveI : Fintype K := Fintype.ofFinite K

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Tactic:
haveI : Finite K := (Nat.card_pos_iff.mp (h ▸ pow_pos h_prime.1.pos n)).2

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this : Finite K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)
-- Mathlib/Order/SuccPred/InitialSeg.lean
theorem isSuccPrelimit_apply_iff (f : α ≤i β) : IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit a
c : α
hb : f c ⋖ f a
⊢ False

Tactic:
rw [f.apply_covBy_apply_iff] at hb

Result:
case mpr.intro
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit a
c : α
hb : c ⋖ a
⊢ False

Proof state:
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Tactic:
constructor <;> intro h b hb

Result:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False

Proof state:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False

Tactic:
obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt

Result:
case mpr.intro
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit a
c : α
hb : f c ⋖ f a
⊢ False

Proof state:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

Tactic:
rw [← f.apply_covBy_apply_iff] at hb

Result:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit (f a)
b : α
hb : f b ⋖ f a
⊢ False

Proof state:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit (f a)
b : α
hb : f b ⋖ f a
⊢ False

Tactic:
exact h _ hb

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsSuccPrelimit a
c : α
hb : c ⋖ a
⊢ False

Tactic:
exact h _ hb

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_type_eq {α : Type u} {β : Type v} {r s} [IsWellOrder α r] [IsWellOrder β s] :
    lift.{max v w} (type r) = lift.{max u w} (type s) ↔ Nonempty (r ≃r s)

Proof state:
case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ :
  isEquivalent
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α, r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r,
      wo := ⋯ }
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≃r s

Tactic:
exact (RelIso.preimage Equiv.ulift r).symm.trans <| f.trans (RelIso.preimage Equiv.ulift s)

Result:
no goals

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

Tactic:
refine Quotient.eq'.trans ⟨?_, ?_⟩ <;> refine fun ⟨f⟩ ↦ ⟨?_⟩

Result:
case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ :
  isEquivalent
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α, r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r,
      wo := ⋯ }
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≃r s

case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Proof state:
case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
exact (RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
lemma additive_of_preserves_binary_products
    [HasBinaryProducts C] [PreservesLimitsOfShape (Discrete WalkingPair) F]
    [F.PreservesZeroMorphisms] : F.Additive

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
⊢ F.Additive

Tactic:
have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts

Result:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
this : HasBinaryBiproducts C
⊢ F.Additive

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
this : HasBinaryBiproducts C
⊢ F.Additive

Tactic:
have := preservesBinaryBiproducts_of_preservesBinaryProducts F

Result:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
this✝ : HasBinaryBiproducts C
this : PreservesBinaryBiproducts F
⊢ F.Additive

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
this✝ : HasBinaryBiproducts C
this : PreservesBinaryBiproducts F
⊢ F.Additive

Tactic:
exact Functor.additive_of_preservesBinaryBiproducts F

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem trace_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    trace (M * N * M⁻¹) = trace N

Proof state:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M * N * M⁻¹).trace = N.trace

Tactic:
rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem single_eq_algebraMap_mul_of [CommSemiring k] [Monoid G] (a : G) (b : k) :
    single a b = algebraMap k (MonoidAlgebra k G) b * of k G a

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : CommSemiring k
inst✝ : Monoid G
a : G
b : k
⊢ single a b = (algebraMap k (MonoidAlgebra k G)) b * (of k G) a

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_iff_not_iff' : Xor' a b ↔ (¬a ↔ b)

Proof state:
a b : Prop
⊢ Xor' a b ↔ (¬a ↔ b)

Tactic:
simp only [← @xor_not_left _ b, not_not]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isOpen_singleton_iff_punctured_nhds (x : X) : IsOpen ({x} : Set X) ↔ 𝓝[≠] x = ⊥

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen {x} ↔ 𝓝[≠] x = ⊥

Tactic:
rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl,
    le_antisymm_iff]

Result:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x

Tactic:
simp [pure_le_nhds x]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- One direction of `inv_mul_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).
-/
lemma inv_mul_le_of_le_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c) : b⁻¹ * a ≤ c

Proof state:
case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ b⁻¹ * a ≤ c

Tactic:
rwa [inv_mul_le_iff₀ hb]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
⊢ b⁻¹ * a ≤ c

Tactic:
obtain rfl | hb := hb.eq_or_lt

Result:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a c : G₀
inst✝ : PosMulMono G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ 0 * c
⊢ 0⁻¹ * a ≤ c

case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ b⁻¹ * a ≤ c

Proof state:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a c : G₀
inst✝ : PosMulMono G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ 0 * c
⊢ 0⁻¹ * a ≤ c

Tactic:
simp [hc]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_eq_zero_of_mutuallySingular {ν' : Measure α} [HaveLebesgueDecomposition μ ν']
    [SigmaFinite ν'] (h : μ ⟂ₘ ν) (hνν' : ν ≪ ν') :
    μ.rnDeriv ν' =ᵐ[ν] 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
filter_upwards [h] with x hx hxt

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
⊢ μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'

Tactic:
have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') :=
  hνν'.ae_le (rnDeriv_restrict μ ν' ht)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0

Tactic:
refine this.trans ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
⊢ (μ.restrict t).rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0