harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/OrderClosed.lean
theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
    [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α]
    {a : α} {f : ι → α} (hlt : ∀ i, f i < a) (hlim : Tendsto f F (𝓝 a)) :
    ⋃ i : ι, Iic (f i) = Iio a

Proof state:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ¬∃ y, f y = a

Tactic:
rintro ⟨i, rfl⟩

Result:
case intro
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
f : ι → α
i : ι
hlt : ∀ (i_1 : ι), f i_1 < f i
hlim : Tendsto f F (𝓝 (f i))
⊢ False

Proof state:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ a ∉ range f

Tactic:
rw [mem_range]

Result:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ¬∃ y, f y = a

Proof state:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ⋃ i, Iic (f i) = Iio a

Tactic:
have obs : a ∉ range f := by
  rw [mem_range]
  rintro ⟨i, rfl⟩
  exact (hlt i).false

Result:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
obs : a ∉ range f
⊢ ⋃ i, Iic (f i) = Iio a

Proof state:
case intro
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
f : ι → α
i : ι
hlt : ∀ (i_1 : ι), f i_1 < f i
hlim : Tendsto f F (𝓝 (f i))
⊢ False

Tactic:
exact (hlt i).false

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem n_lt_a_pow : ∀ n : ℕ, n < a ^ n
  | 0 => Nat.le_refl 1
  | n + 1 => by
    have IH := n_lt_a_pow n
    have : a ^ n + a ^ n ≤ a ^ n * a

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ n + 1 < a ^ (n + 1)

Tactic:
have IH := n_lt_a_pow n

Result:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ n + 1 < a ^ (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n * a

Tactic:
refine lt_of_lt_of_le ?_ this

Result:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n + a ^ n

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ a ^ n + a ^ n ≤ a ^ n * a

Tactic:
rw [← mul_two]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ a ^ n * 2 ≤ a ^ n * a

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ n + 1 < a ^ (n + 1)

Tactic:
have : a ^ n + a ^ n ≤ a ^ n * a := by
  rw [← mul_two]
  exact Nat.mul_le_mul_left _ a1

Result:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ a ^ n * 2 ≤ a ^ n * a

Tactic:
exact Nat.mul_le_mul_left _ a1

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ (n + 1)

Tactic:
simp only [_root_.pow_succ, gt_iff_lt]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n * a

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n + a ^ n

Tactic:
exact add_lt_add_of_lt_of_le IH (lt_of_le_of_lt (Nat.zero_le _) IH)

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem induction (P : solvableByRad F E → Prop)
    (base : ∀ α : F, P (algebraMap F (solvableByRad F E) α))
    (add : ∀ α β : solvableByRad F E, P α → P β → P (α + β))
    (neg : ∀ α : solvableByRad F E, P α → P (-α))
    (mul : ∀ α β : solvableByRad F E, P α → P β → P (α * β))
    (inv : ∀ α : solvableByRad F E, P α → P α⁻¹)
    (rad : ∀ α : solvableByRad F E, ∀ n : ℕ, n ≠ 0 → P (α ^ n) → P α) (α : solvableByRad F E) :
    P α

Proof state:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : F), ∃ β, ↑β = (algebraMap F E) α ∧ P β

Tactic:
exact fun α => ⟨algebraMap F (solvableByRad F E) α, rfl, base α⟩

Result:
no goals

Proof state:
case h.e'_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : ↥(solvableByRad F E)
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ ⟨α, ⋯⟩ ^ n = α₀

Tactic:
exact Subtype.ext (Eq.trans ((solvableByRad F E).coe_pow _ n) hα₀.symm)

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : ↥(solvableByRad F E)), P α

Tactic:
suffices ∀ α : E, IsSolvableByRad F α → ∃ β : solvableByRad F E, ↑β = α ∧ P β by
  intro α
  obtain ⟨α₀, hα₀, Pα⟩ := this α (Subtype.mem α)
  convert Pα
  exact Subtype.ext hα₀.symm

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : ↥(solvableByRad F E) → Prop
base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)
add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)
neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)
mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)
inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹
rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
-- Mathlib/Order/Filter/AtTopBot/Finset.lean
theorem tendsto_atTop_finset_of_monotone [Preorder β] {f : β → Finset α} (h : Monotone f)
    (h' : ∀ x : α, ∃ n, x ∈ f n) : Tendsto f atTop atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}

Tactic:
rcases h' a with ⟨b, hb⟩

Result:
case intro
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ ∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}

Tactic:
intro a

Result:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ Tendsto f atTop atTop

Tactic:
simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]

Result:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ ∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}

Proof state:
case intro
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}

Tactic:
exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem support_single_add {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
    support (single a b + f) = cons a f.support ha

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (single a b + f).support = cons a f.support ha

Tactic:
classical
have H := support_single_ne_zero a hb
rw [support_add_eq, H, cons_eq_insert, insert_eq]
rwa [H, disjoint_singleton_left]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (single a b + f).support = cons a f.support ha

Tactic:
rw [support_add_eq, H, cons_eq_insert, insert_eq]

Result:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint (single a b).support f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint (single a b).support f.support

Tactic:
rwa [H, disjoint_singleton_left]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (single a b + f).support = cons a f.support ha

Tactic:
have H := support_single_ne_zero a hb

Result:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (single a b + f).support = cons a f.support ha
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_eq_zero {m : M} (s : S) : mk' f m s = 0 ↔ f m = 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ f m = 0

Tactic:
rw [mk'_eq_iff, smul_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma Nonempty.zero_smul (ht : t.Nonempty) : (0 : Finset α) • t = 0 :=
  t.zero_smul_subset.antisymm <| by simpa [mem_smul] using ht

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Finset β
ht : t.Nonempty
⊢ 0 ⊆ 0 • t

Tactic:
simpa [mem_smul] using ht

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem continuous_transReflReparamAux : Continuous transReflReparamAux

Proof state:
⊢ Continuous transReflReparamAux

Tactic:
refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_ <;>
  [continuity; continuity; continuity; continuity; skip]

Result:
case refine_5

⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1

Proof state:
case refine_5

⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1

Tactic:
intro x hx

Result:
case refine_5
x : ↑I
hx : ↑x = 1 / 2
⊢ 2 * ↑x = 1

Proof state:
case refine_5
x : ↑I
hx : ↑x = 1 / 2
⊢ 2 * ↑x = 1

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- The `LSeries` of `f` is zero for large real arguments if and only if either `f n = 0`
for all `n ≠ 0` or the L-series converges nowhere. -/
lemma LSeries_eventually_eq_zero_iff' {f : ℕ → ℂ} :
    (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] 0 ↔ (∀ n ≠ 0, f n = 0) ∨ abscissaOfAbsConv f = ⊤

Proof state:
case neg.refine_1.ind
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
⊢ F n = 0

Tactic:
suffices Tendsto (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) atTop (nhds (F n)) by
  replace this := this.congr' <| H' n
  simp only [tendsto_const_nhds_iff] at this
  exact this.symm

Result:
case neg.refine_1.ind
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
⊢ Tendsto (fun x => ↑n ^ ↑x * LSeries F ↑x) atTop (nhds (F n))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[i+1]! = l[i]!

Proof state:
case neg
α : Type u_1
a : α
i : Nat
inst✝ : Inhabited α
l : List α
h : ¬i < l.length
⊢ (a :: l)[i + 1]! = l[i]!

Tactic:
rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case pos
α : Type u_1
a : α
i : Nat
inst✝ : Inhabited α
l : List α
h : i < l.length
⊢ (a :: l)[i + 1]! = l[i]!

Tactic:
rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
α : Type u_1
a : α
i : Nat
inst✝ : Inhabited α
l : List α
⊢ (a :: l)[i + 1]! = l[i]!

Tactic:
by_cases h : i < l.length

Result:
case pos
α : Type u_1
a : α
i : Nat
inst✝ : Inhabited α
l : List α
h : i < l.length
⊢ (a :: l)[i + 1]! = l[i]!

case neg
α : Type u_1
a : α
i : Nat
inst✝ : Inhabited α
l : List α
h : ¬i < l.length
⊢ (a :: l)[i + 1]! = l[i]!
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem le_einfsep_pair : edist x y ⊓ edist y x ≤ ({x, y} : Set α).einfsep

Proof state:
α : Type u_1
inst✝ : EDist α
x y : α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 = y →
      ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1

Tactic:
rintro a (rfl | rfl) b (rfl | rfl) hab <;> (try simp only [le_refl, true_or, or_true]) <;>
  contradiction

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
try simp only [le_refl, true_or, or_true]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : EDist α
x y : α
⊢ edist x y ⊓ edist y x ≤ {x, y}.einfsep

Tactic:
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]

Result:
α : Type u_1
inst✝ : EDist α
x y : α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 = y →
      ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1

Proof state:
case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
simp only [le_refl, true_or, or_true]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem leftAdjointUniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
  conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
  conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
  Category.assoc]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit

Tactic:
ext x

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x

Tactic:
simp

Result:
no goals

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_inter_mul_diff' (t : Set α) (h : (s ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
rw [← finprod_mem_union', inter_union_diff]

Result:
case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ Disjoint (s ∩ t) (s \ t)

case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s ∩ t ∩ mulSupport f).Finite

case ht
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s \ t ∩ mulSupport f).Finite

Proof state:
case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ s ∩ t ⊓ s \ t ≤ ⊥

Tactic:
exact fun x hx => hx.2.2 hx.1.2

Result:
no goals

Proof state:
case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ Disjoint (s ∩ t) (s \ t)

Tactic:
rw [disjoint_iff_inf_le]

Result:
case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ s ∩ t ⊓ s \ t ≤ ⊥

Proof state:
case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s ∩ t ∩ mulSupport f).Finite

case ht
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s \ t ∩ mulSupport f).Finite

Tactic:
exacts [h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
lemma sdiff_mem (ha : a ∈ L) (hb : b ∈ L) : a \ b ∈ L

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a \ b ∈ L

Tactic:
simpa [sdiff_eq] using L.infClosed ha (compl_mem hb)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Integral.lean
theorem lintegral_rpow_eq_lintegral_meas_le_mul :
    ∫⁻ ω, ENNReal.ofReal (f ω ^ p) ∂μ =
      ENNReal.ofReal p * ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ

Tactic:
congr with ω

Result:
case e_f.h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
ω : α
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : t ∈ Ioi 0
⊢ 0 ≤ g t

Tactic:
exact Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)

Result:
no goals
-- Mathlib/LinearAlgebra/JordanChevalley.lean
theorem exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow {P : K[X]} {k : ℕ}
    (sep : P.Separable) (nil : minpoly K f ∣ P ^ k) :
    ∃ᵉ (n ∈ adjoin K {f}) (s ∈ adjoin K {f}), IsNilpotent n ∧ IsSemisimple s ∧ f = n + s

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
obtain ⟨⟨s, mem⟩, ⟨⟨k, hk⟩, hss⟩, -⟩ := existsUnique_nilpotent_sub_and_aeval_eq_zero nil' sep'

Result:
case intro.mk.intro.intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ adjoin K {f}
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
-- Mathlib/Data/PNat/Prime.lean
theorem gcd_eq_left_iff_dvd {m n : ℕ+} : m ∣ n ↔ m.gcd n = m

Proof state:
m n : ℕ+
⊢ ↑m ∣ ↑n ↔ m.gcd n = m

Tactic:
rw [Nat.gcd_eq_left_iff_dvd]

Result:
m n : ℕ+
⊢ (↑m).gcd ↑n = ↑m ↔ m.gcd n = m

Proof state:
m n : ℕ+
⊢ m ∣ n ↔ m.gcd n = m

Tactic:
rw [dvd_iff]

Result:
m n : ℕ+
⊢ ↑m ∣ ↑n ↔ m.gcd n = m

Proof state:
m n : ℕ+
⊢ (↑m).gcd ↑n = ↑m ↔ ↑(m.gcd n) = ↑m

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ+
⊢ (↑m).gcd ↑n = ↑m ↔ m.gcd n = m

Tactic:
rw [← coe_inj]

Result:
m n : ℕ+
⊢ (↑m).gcd ↑n = ↑m ↔ ↑(m.gcd n) = ↑m
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_leftUnitor {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : p ≫ f ≅ pf) :
    p ◁ (λ_ f) ≪≫ η_f = normalizeIsoComp (ρ_ p) η_f :=
  Iso.ext (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ λ_ f ≪≫ η_f).hom = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem eventually_homothety_mem_of_mem_interior (x : Q) {s : Set Q} {y : Q} (hy : y ∈ interior s) :
    ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s

Proof state:
case h
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y = x
⊢ 0 < 1 ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < 1} → (homothety x x_1) y ∈ s

Tactic:
simp [h.symm, interior_subset hy]

Result:
no goals