harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Field/Basic.lean
lemma norm_commutator_units_sub_one_le (a b : αˣ) :
    ‖(a * b * a⁻¹ * b⁻¹).val - 1‖ ≤ 2 * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ * ‖a.val - 1‖ * ‖b.val - 1‖ :=
  calc
    ‖(a * b * a⁻¹ * b⁻¹).val - 1‖ = ‖(a * b - b * a) * a⁻¹.val * b⁻¹.val‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖ = ‖(↑a * ↑b - ↑b * ↑a) * ↑a⁻¹ * ↑b⁻¹‖

Tactic:
simp [sub_mul, *]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
simp_rw [sub_one_mul, mul_sub_one]

Result:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
abel_nf

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ (‖↑a - 1‖ * ‖↑b - 1‖ + ‖↑b - 1‖ * ‖↑a - 1‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = 2 * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ * ‖↑a - 1‖ * ‖↑b - 1‖

Tactic:
ring

Result:
no goals

Proof state:
case h.h
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ ≤ ‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖

Tactic:
exact norm_sub_le ..

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ (‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ ≤
    (‖↑a - 1‖ * ‖↑b - 1‖ + ‖↑b - 1‖ * ‖↑a - 1‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
gcongr <;> exact norm_mul_le ..

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ ≤
    (‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
gcongr

Result:
case h.h
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ ≤ ‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem finRotate_succ_eq_decomposeFin {n : ℕ} :
    finRotate n.succ = decomposeFin.symm (1, finRotate n)

Proof state:
case H.h.zero
i : Fin (Nat.succ 0)
⊢ ↑((finRotate (Nat.succ 0)) i) = ↑((decomposeFin.symm (1, finRotate 0)) i)

Tactic:
simp

Result:
no goals

Proof state:
case H.h.succ
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) i) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i)

Tactic:
refine Fin.cases ?_ (fun i => ?_) i

Result:
case H.h.succ.refine_1
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) 0) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) 0)

case H.h.succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ ↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)

Proof state:
case pos
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i.succ + 1 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
  if_neg h, Fin.val_zero, Fin.val_one,
  swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]

Result:
no goals

Proof state:
case H.h.succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑i.succ + 1) = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
split_ifs with h

Result:
case pos
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i.succ + 1 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Proof state:
case H.h.succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ ↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)

Tactic:
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]

Result:
case H.h.succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑i.succ + 1) = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Proof state:
n : ℕ
⊢ finRotate n.succ = decomposeFin.symm (1, finRotate n)

Tactic:
ext i

Result:
case H.h
n : ℕ
i : Fin n.succ
⊢ ↑((finRotate n.succ) i) = ↑((decomposeFin.symm (1, finRotate n)) i)

Proof state:
case H.h
n : ℕ
i : Fin n.succ
⊢ ↑((finRotate n.succ) i) = ↑((decomposeFin.symm (1, finRotate n)) i)

Tactic:
cases n

Result:
case H.h.zero
i : Fin (Nat.succ 0)
⊢ ↑((finRotate (Nat.succ 0)) i) = ↑((decomposeFin.symm (1, finRotate 0)) i)

case H.h.succ
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) i) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i)

Proof state:
case H.h.succ.refine_1
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) 0) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) 0)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma mem_subgroup_orbit_iff {H : Subgroup G} {x : α} {a b : orbit G x} :
    a ∈ MulAction.orbit H b ↔ (a : α) ∈ MulAction.orbit H (b : α)

Proof state:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑g • b ∈ orbit (↥H) b

Tactic:
exact MulAction.mem_orbit _ g

Result:
no goals

Proof state:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : a ∈ orbit (↥H) b
⊢ ↑a ∈ orbit ↥H ↑b

Tactic:
rcases h with ⟨g, rfl⟩

Result:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑((fun m => m • b) g) ∈ orbit ↥H ↑b

Proof state:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : (fun m => m • ↑b) g = ↑a
⊢ a ∈ orbit (↥H) b

Tactic:
dsimp at h

Result:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ orbit (↥H) b

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
⊢ a ∈ orbit (↥H) b ↔ ↑a ∈ orbit ↥H ↑b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : a ∈ orbit (↥H) b
⊢ ↑a ∈ orbit ↥H ↑b

case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : ↑a ∈ orbit ↥H ↑b
⊢ a ∈ orbit (↥H) b

Proof state:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : ↑a ∈ orbit ↥H ↑b
⊢ a ∈ orbit (↥H) b

Tactic:
rcases h with ⟨g, h⟩

Result:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : (fun m => m • ↑b) g = ↑a
⊢ a ∈ orbit (↥H) b

Proof state:
case refine_1.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑((fun m => m • b) g) ∈ orbit ↥H ↑b

Tactic:
exact MulAction.mem_orbit _ g

Result:
no goals

Proof state:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : ↑g • b = a
⊢ a ∈ orbit (↥H) b

Tactic:
subst h

Result:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑g • b ∈ orbit (↥H) b

Proof state:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ orbit (↥H) b

Tactic:
erw [← orbit.coe_smul, ← Subtype.ext_iff] at h

Result:
case refine_2.intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : ↑g • b = a
⊢ a ∈ orbit (↥H) b
-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem submodulesRingBasis : SubmodulesRingBasis
    (fun (r : R⁰) ↦ Submodule.span (R_hat R K) {((r : R) : FiniteAdeleRing R K)}) where
  inter i j := ⟨i * j, by
    push_cast
    simp only [le_inf_iff, Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
    exact ⟨⟨((j : R) : R_hat R K), by rw [mul_comm]; rfl⟩, ⟨((i : R) : R_hat R K), rfl⟩⟩⟩
  leftMul a r

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
i j : ↥R⁰
⊢ Submodule.span (R_hat R K) {↑↑(i * j)} ≤ Submodule.span (R_hat R K) {↑↑i} ⊓ Submodule.span (R_hat R K) {↑↑j}

Tactic:
push_cast

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
i j : ↥R⁰
⊢ Submodule.span (R_hat R K) {↑↑i * ↑↑j} ≤ Submodule.span (R_hat R K) {↑↑i} ⊓ Submodule.span (R_hat R K) {↑↑j}
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem mconv_zero (μ : Measure M) : (0 : Measure M) ∗ μ = (0 : Measure M)

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ map (fun x => x.1 * x.2) (Measure.prod 0 μ) = 0

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ 0 ∗ μ = 0

Tactic:
unfold mconv

Result:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ map (fun x => x.1 * x.2) (Measure.prod 0 μ) = 0
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_congr (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖

Tactic:
subst c₂

Result:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂

Tactic:
simp only [IsBigOWith_def]

Result:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖

Proof state:
case h
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖

Tactic:
rw [e₁, e₂]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖

Tactic:
filter_upwards [hf, hg] with _ e₁ e₂

Result:
case h
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖

Tactic:
apply Filter.eventually_congr

Result:
case h
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
-- Mathlib/NumberTheory/FunctionField.lean
theorem functionField_iff (Fqt : Type*) [Field Fqt] [Algebra Fq[X] Fqt]
    [IsFractionRing Fq[X] Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra Fq[X] F]
    [IsScalarTower Fq[X] Fqt F] [IsScalarTower Fq[X] (RatFunc Fq) F] :
    FunctionField Fq F ↔ FiniteDimensional Fqt F

Proof state:
case mpr
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FiniteDimensional Fqt F
⊢ FunctionField Fq F

Tactic:
let b := Module.finBasis Fqt F

Result:
case mpr
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (Module.finrank Fqt F)) Fqt F := Module.finBasis Fqt F
⊢ FunctionField Fq F

Proof state:
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ e c • x = c • x

Tactic:
rw [Algebra.smul_def, Algebra.smul_def]

Result:
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ (algebraMap Fqt F) (e c) * x = (algebraMap (RatFunc Fq) F) c * x
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem lt_nmul_iff : c < a ⨳ b ↔ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'

Proof state:
case refine_2.intro.intro.intro.intro
a b c a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ c < a ⨳ b

Tactic:
have := h.trans_lt (nmul_nadd_lt ha hb)

Result:
case refine_2.intro.intro.intro.intro
a b c a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : c ♯ a' ⨳ b' < a ⨳ b ♯ a' ⨳ b'
⊢ c < a ⨳ b

Proof state:
case refine_2.intro.intro.intro.intro
a b c a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : c ♯ a' ⨳ b' < a ⨳ b ♯ a' ⨳ b'
⊢ c < a ⨳ b

Tactic:
rwa [nadd_lt_nadd_iff_right] at this

Result:
no goals

Proof state:
a b c : Ordinal.{u}
⊢ c < a ⨳ b ↔ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
a b c : Ordinal.{u}
h : c < a ⨳ b
⊢ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'

case refine_2
a b c : Ordinal.{u}
⊢ (∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b') → c < a ⨳ b

Proof state:
case refine_1
a b c : Ordinal.{u}
h : c < a ⨳ b
⊢ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'

Tactic:
rw [nmul] at h

Result:
case refine_1
a b c : Ordinal.{u}
h : c < sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
⊢ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'

Proof state:
case refine_2
a b c : Ordinal.{u}
⊢ (∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b') → c < a ⨳ b

Tactic:
rintro ⟨a', ha, b', hb, h⟩

Result:
case refine_2.intro.intro.intro.intro
a b c a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ c < a ⨳ b

Proof state:
case refine_1
a b c : Ordinal.{u}
h : c < sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
⊢ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'

Tactic:
simpa using not_mem_of_lt_csInf h ⟨0, fun _ _ => bot_le⟩

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_associator_inv (X Y Z : C) :
    F.map (α_ X Y Z).inv =
      δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫
        (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).inv =
    δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
rw [← cancel_epi (F.map (α_ X Y Z).hom), Iso.map_hom_inv_id, map_associator,
  assoc, assoc, assoc, assoc, OplaxMonoidal.associativity_inv_assoc,
  whiskerRight_δ_μ_assoc, δ_μ, comp_id, LaxMonoidal.associativity_inv,
  Iso.hom_inv_id_assoc, whiskerRight_δ_μ_assoc, δ_μ]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_one {n : ℕ} (hn : 0 < n) :
    term n 1 = (log (n + 1) - log n) -  1 / (n + 1)

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ContinuousOn (fun x => x ^ 2) (uIcc (↑n) (↑n + 1))

Tactic:
fun_prop

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2 =
    log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2)

Tactic:
congr 2

Result:
case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2 = ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2)

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
  rpow_neg_one, ← one_div]

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2) = log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
rw [integral_rpow]

Result:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -1 < -2 ∨ -2 ≠ -1 ∧ 0 ∉ uIcc (↑n) (↑n + 1)

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x - ↑n) * (x * x ^ 2) = (x ^ 2 - x * ↑n) * x ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean
@[to_additive] lemma le_iff_exists_one_le_mul [MulLeftMono α]
    [MulLeftReflectLE α] : a ≤ b ↔ ∃ c, 1 ≤ c ∧ a * c = b :=
  ⟨exists_one_le_mul_of_le, by rintro ⟨c, hc, rfl⟩; exact le_mul_of_one_le_right' hc⟩

Proof state:
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
⊢ (∃ c, 1 ≤ c ∧ a * c = b) → a ≤ b

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case intro.intro
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
c : α
hc : 1 ≤ c
⊢ a ≤ a * c

Proof state:
case intro.intro
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
c : α
hc : 1 ≤ c
⊢ a ≤ a * c

Tactic:
exact le_mul_of_one_le_right' hc

Result:
no goals
-- Mathlib/Order/Disjointed.lean
lemma disjointed_succ (f : ι → α) {i : ι} (hi : ¬IsMax i) :
    disjointed f (succ i) = f (succ i) \ partialSups f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f) i

Tactic:
rw [disjointed_apply, partialSups_apply, sup'_eq_sup]

Result:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f

Proof state:
case e_a.e_s.h
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
m : ι
⊢ m ∈ Iio (succ i) ↔ m ∈ Iic i

Tactic:
simpa only [mem_Iio, mem_Iic] using lt_succ_iff_of_not_isMax hi

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f

Tactic:
congr 2 with m

Result:
case e_a.e_s.h
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
m : ι
⊢ m ∈ Iio (succ i) ↔ m ∈ Iic i
-- Mathlib/MeasureTheory/Covering/Vitali.lean
theorem exists_disjoint_subfamily_covering_enlargement (B : ι → Set α) (t : Set ι) (δ : ι → ℝ)
    (τ : ℝ) (hτ : 1 < τ) (δnonneg : ∀ a ∈ t, 0 ≤ δ a) (R : ℝ) (δle : ∀ a ∈ t, δ a ≤ R)
    (hne : ∀ a ∈ t, (B a).Nonempty) :
    ∃ u ⊆ t,
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b

Proof state:
case inr.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x => x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
x : ℝ
xA : x ∈ δ '' A
hx : m / τ < x
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩

Result:
case inr.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x => x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
hx : m / τ < δ a'
⊢ ∃ a' ∈ A, m / τ ≤ δ a'