harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem degree_div_lt (hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q = 0
⊢ False

Tactic:
simp [hq0] at hq

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
⊢ (p / q).degree < p.degree

Tactic:
have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p / q).degree < p.degree

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ 0 < q.degree

Tactic:
exact hq

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p / q).degree < p.degree

Tactic:
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p /ₘ (q * C q.leadingCoeff⁻¹)).degree < p.degree

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p /ₘ (q * C q.leadingCoeff⁻¹)).degree < p.degree

Tactic:
exact degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp
  (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ 0 < (q * C q.leadingCoeff⁻¹).degree

Tactic:
rw [degree_mul_leadingCoeff_inv _ hq0]

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ 0 < q.degree
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
private lemma fintype_cliqueNum_bddAbove [Fintype α] : BddAbove {n | ∃ s, G.IsNClique n s}

Proof state:
case h.intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
y : ℕ
s : Finset α
syc : G.IsNClique y s
⊢ y ≤ Fintype.card α

Tactic:
rw [isNClique_iff] at syc

Result:
case h.intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ y ≤ Fintype.card α

Proof state:
case h
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ Fintype.card α ∈ upperBounds {n | ∃ s, G.IsNClique n s}

Tactic:
rintro y ⟨s, syc⟩

Result:
case h.intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
y : ℕ
s : Finset α
syc : G.IsNClique y s
⊢ y ≤ Fintype.card α

Proof state:
case h.intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ y ≤ Fintype.card α

Tactic:
rw [← syc.right]

Result:
case h.intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ #s ≤ Fintype.card α

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ BddAbove {n | ∃ s, G.IsNClique n s}

Tactic:
use Fintype.card α

Result:
case h
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ Fintype.card α ∈ upperBounds {n | ∃ s, G.IsNClique n s}

Proof state:
case h.intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ #s ≤ Fintype.card α

Tactic:
exact Finset.card_le_card (Finset.subset_univ s)

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_div {a b : ℝ≥0∞} (htop : b ≠ ∞ ∨ a ≠ ∞) (hzero : b ≠ 0 ∨ a ≠ 0) :
    (a / b)⁻¹ = b / a

Proof state:
a b : ℝ≥0∞
htop : b ≠ ⊤ ∨ a ≠ ⊤
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [← ENNReal.inv_ne_zero] at htop

Result:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ⊤
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Proof state:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ⊤
hzero : b⁻¹ ≠ ⊤ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]

Result:
no goals

Proof state:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ⊤
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [← ENNReal.inv_ne_top] at hzero

Result:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ⊤
hzero : b⁻¹ ≠ ⊤ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem carry_zero : carry 0 x y c = c

Proof state:
w✝ : Nat
x y : BitVec w✝
c : Bool
⊢ carry 0 x y c = c

Tactic:
cases c <;> simp [carry, mod_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_period [AddGroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) :
    Periodic f (c₁ - c₂) := fun x => by
  rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x

Tactic:
rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem unbot_eq_iff {a : WithBot α} {b : α} (h : a ≠ ⊥) :
    a.unbot h = b ↔ a = b

Proof state:
α : Type u_1
a : WithBot α
b : α
h : a ≠ ⊥
⊢ a.unbot h = b ↔ a = ↑b

Tactic:
induction a

Result:
case bot
α : Type u_1
b : α
h : ⊥ ≠ ⊥
⊢ ⊥.unbot h = b ↔ ⊥ = ↑b

case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b

Proof state:
case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b

Tactic:
simp

Result:
no goals

Proof state:
case bot
α : Type u_1
b : α
h : ⊥ ≠ ⊥
⊢ ⊥.unbot h = b ↔ ⊥ = ↑b

Tactic:
simpa using h rfl

Result:
no goals
-- Mathlib/Topology/Gluing.lean
theorem rel_equiv : Equivalence D.Rel :=
  ⟨fun x => ⟨inv (D.f _ _) x.2, IsIso.inv_hom_id_apply (D.f x.fst x.fst) _,
    -- Use `elementwise_of%` elaborator instead of `IsIso.inv_hom_id_apply` to work around
    -- `ConcreteCategory`/`HasForget` mismatch:
    by simp [elementwise_of% IsIso.inv_hom_id (D.f x.fst x.fst)]⟩, by
    rintro a b ⟨x, e₁, e₂⟩
    exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩, by
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ ⟨x, e₁, e₂⟩
    rintro ⟨y, e₃, e₄⟩
    let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩
    have eq₁ : (D.t j i) ((pullback.fst _ _ : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x

Proof state:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)

Result:
case a
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' k j i ≫ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    D.t' k j i ≫ pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.iInf_ker_openCover_map_comp_apply
    (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) (U : Y.affineOpens) :
    ⨅ i, (𝒰.map i ≫ f).ker.ideal U = f.ker.ideal U

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
⊢ (CommRingCat.Hom.hom (f.app ↑U)) s = 0

Tactic:
apply X.IsSheaf.section_ext

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
⊢ ∀ x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U)),
    ∃ V,
      ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
        x ∈ V ∧
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
            (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
⊢ s ∈ f.ker.ideal U

Tactic:
simp only [Hom.ker_apply, RingHom.mem_ker]

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
⊢ (CommRingCat.Hom.hom (f.app ↑U)) s = 0

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
⊢ ∀ x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U)),
    ∃ V,
      ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
        x ∈ V ∧
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
            (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0

Tactic:
rintro x hxU

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
      x ∈ V ∧
        (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0
-- Mathlib/LinearAlgebra/Dual.lean
@[simp]
lemma dualCoannihilator_range_eq_ker_flip (B : M →ₗ[R] M' →ₗ[R] R) :
    (range B).dualCoannihilator = LinearMap.ker B.flip

Proof state:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
x : M'
⊢ x ∈ (range B).dualCoannihilator ↔ x ∈ ker B.flip

Tactic:
simp [LinearMap.ext_iff (f := B.flip x)]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
⊢ (range B).dualCoannihilator = ker B.flip

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
x : M'
⊢ x ∈ (range B).dualCoannihilator ↔ x ∈ ker B.flip
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
@[simp] lemma inv_smul_finset_distrib₀ (a : α) (s : Finset α) : (a • s)⁻¹ = s⁻¹ <• a⁻¹

Proof state:
case inr.h
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (a •> s)⁻¹ ↔ a✝ ∈ s⁻¹ <• a⁻¹

Tactic:
simp only [mem_inv', ne_eq, not_false_eq_true, ← inv_smul_mem_iff₀, smul_eq_mul,
MulOpposite.op_inv, inv_eq_zero, MulOpposite.op_eq_zero_iff, inv_inv,
MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
ext

Result:
case inr.h
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (a •> s)⁻¹ ↔ a✝ ∈ s⁻¹ <• a⁻¹

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Proof state:
case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma whiskerLeft_id (X Y : LocalizedMonoidal L W ε) :
    X ◁ (𝟙 Y) = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
⊢ X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem IsStrongLimit.isSuccLimit {c} (H : IsStrongLimit c) : IsSuccLimit c

Proof state:
c : Cardinal.{u_1}
H : c.IsStrongLimit
⊢ c ≠ 0 ∧ IsSuccPrelimit c

Tactic:
exact ⟨H.ne_zero, isSuccPrelimit_of_succ_lt fun x h ↦
  (succ_le_of_lt <| cantor x).trans_lt (H.two_power_lt h)⟩

Result:
no goals

Proof state:
c : Cardinal.{u_1}
H : c.IsStrongLimit
⊢ IsSuccLimit c

Tactic:
rw [Cardinal.isSuccLimit_iff]

Result:
c : Cardinal.{u_1}
H : c.IsStrongLimit
⊢ c ≠ 0 ∧ IsSuccPrelimit c
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma mem_dynEntourage {T : X → X} {U : Set (X × X)} {n : ℕ} {x y : X} :
    (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
x y : X
⊢ (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

Tactic:
simp [dynEntourage]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
theorem le_norm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f‖ ≤ ‖flip f‖ :=
  f.opNorm_le_bound₂ (norm_nonneg f.flip) fun x y => by
    rw [mul_right_comm]
    exact (flip f).le_opNorm₂ y x

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖y‖ * ‖x‖

Tactic:
exact (flip f).le_opNorm₂ y x

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖x‖ * ‖y‖

Tactic:
rw [mul_right_comm]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖y‖ * ‖x‖
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atTop_of_pos (hr : 0 < r) :
    Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalSemiring_injective :
    Function.Injective (@toNonUnitalSemiring R)

Proof state:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : toNonUnitalSemiring = toNonUnitalSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : toNonUnitalSemiring = toNonUnitalSemiring
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : toNonUnitalSemiring = toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : toNonUnitalSemiring = toNonUnitalSemiring
⊢ a₁✝ = a₂✝
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_add_right' (a b : α) : toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_add_zsmul' hp a b 1

Result:
no goals
-- Mathlib/Algebra/Equiv/TransferInstance.lean
lemma algebraMap_def (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) :
    (@algebraMap R α _ (Equiv.semiring e) (Equiv.algebra R e)) r = e.symm ((algebraMap R β) r)

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
⊢ (algebraMap R α) r = e.symm ((algebraMap R β) r)

Tactic:
let _ := Equiv.semiring e

Result:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝ : Semiring α := e.semiring
⊢ (algebraMap R α) r = e.symm ((algebraMap R β) r)

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝¹ : Semiring α := e.semiring
x✝ : Algebra R α := Equiv.algebra R e
⊢ (algebraMap R α) r = e.symm ((algebraMap R β) r)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one]

Result:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝¹ : Semiring α := e.semiring
x✝ : Algebra R α := Equiv.algebra R e
⊢ r • 1 = e.symm (r • 1)

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝ : Semiring α := e.semiring
⊢ (algebraMap R α) r = e.symm ((algebraMap R β) r)

Tactic:
let _ := Equiv.algebra R e

Result:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝¹ : Semiring α := e.semiring
x✝ : Algebra R α := Equiv.algebra R e
⊢ (algebraMap R α) r = e.symm ((algebraMap R β) r)

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝¹ : Semiring α := e.semiring
x✝ : Algebra R α := Equiv.algebra R e
⊢ e.symm (r • e 1) = e.symm (r • 1)

Tactic:
simp only [Equiv.one_def, apply_symm_apply]

Result:
no goals

Proof state:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝¹ : Semiring α := e.semiring
x✝ : Algebra R α := Equiv.algebra R e
⊢ r • 1 = e.symm (r • 1)

Tactic:
show e.symm (r • e 1) = e.symm (r • 1)

Result:
α : Type u
β : Type v
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
r : R
x✝¹ : Semiring α := e.semiring
x✝ : Algebra R α := Equiv.algebra R e
⊢ e.symm (r • e 1) = e.symm (r • 1)
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma monotoneOn_of_pred_le (hs : s.OrdConnected)
    (hf : ∀ a, ¬ IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a) : MonotoneOn f s

Proof state:
case intro.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
ha : pred^[0] b ∈ s
⊢ f (pred^[0] b) ≤ f b

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
theorem ae_not_liouvilleWith : ∀ᵐ x, ∀ p > (2 : ℝ), ¬LiouvilleWith p x

Proof state:
⊢ ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x

Tactic:
simpa only [ae_iff, not_forall, Classical.not_not, setOf_exists] using
  volume_iUnion_setOf_liouvilleWith

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma finrank_of_isSplittingField_X_pow_sub_C : Module.finrank K L = n

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
⊢ Module.finrank K L = n

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Result:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
hn : 0 < n
⊢ Module.finrank K L = n

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this : FiniteDimensional K L
⊢ Module.finrank K L = n

Tactic:
have := isGalois_of_isSplittingField_X_pow_sub_C hζ H L

Result:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
⊢ Module.finrank K L = n

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
⊢ Module.finrank K L = n

Tactic:
have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a)

Result:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this : FiniteDimensional K L
⊢ Module.finrank K L = n

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
hn : 0 < n
⊢ Module.finrank K L = n

Tactic:
have : NeZero n := ⟨ne_zero_of_irreducible_X_pow_sub_C H⟩

Result:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
hn : 0 < n
this : NeZero n
⊢ Module.finrank K L = n

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
hn : 0 < n
this : NeZero n
⊢ Module.finrank K L = n

Tactic:
rw [← IsGalois.card_aut_eq_finrank, Fintype.card_congr ((autEquivZmod H L <|
  (mem_primitiveRoots hn).mp hζ.choose_spec).toEquiv.trans Multiplicative.toAdd), ZMod.card]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem centroid_map (e : ι₂ ↪ ι) (p : ι → P) :
    (s₂.map e).centroid k p = s₂.centroid k (p ∘ e)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
p : ι → P
⊢ centroid k (map e s₂) p = centroid k s₂ (p ∘ ⇑e)

Tactic:
simp [centroid_def, affineCombination_map, centroidWeights]

Result:
no goals