harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem unifIntegrable_of (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → β}
    (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    (h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0,
      ∀ i, eLpNorm ({ x | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
    UnifIntegrable f p μ

Proof state:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
rw [Set.indicator_of_not_mem hfx, Set.indicator_of_not_mem]

Result:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
-- Mathlib/SetTheory/Lists.lean
theorem mem_of_subset' {a} : ∀ {l₁ l₂ : Lists' α true} (_ : l₁ ⊆ l₂) (_ : a ∈ l₁.toList), a ∈ l₂
  | nil, _, Lists'.Subset.nil, h => by cases h
  | cons' a0 l0, l₂, s, h => by
    obtain - | ⟨e, m, s⟩ := s
    simp only [toList, Sigma.eta, List.find?, List.mem_cons] at h
    rcases h with (rfl | h)
    · exact ⟨_, m, e⟩
    · exact mem_of_subset' s h

Proof state:
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
h : a = a✝ ∨ a ∈ l0.toList
⊢ a ∈ l₂

Tactic:
rcases h with (rfl | h)

Result:
case cons.inl
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
e : a ~ a'✝
⊢ a ∈ l₂

case cons.inr
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
h : a ∈ l0.toList
⊢ a ∈ l₂

Proof state:
case cons.inl
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
e : a ~ a'✝
⊢ a ∈ l₂

Tactic:
exact ⟨_, m, e⟩

Result:
no goals

Proof state:
α : Type u_1
a : Lists α
x✝ : Lists' α true
h : a ∈ nil.toList
⊢ a ∈ x✝

Tactic:
cases h

Result:
no goals

Proof state:
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
h : a ∈ (a✝.snd.cons' l0).toList
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
⊢ a ∈ l₂

Tactic:
simp only [toList, Sigma.eta, List.find?, List.mem_cons] at h

Result:
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
h : a = a✝ ∨ a ∈ l0.toList
⊢ a ∈ l₂

Proof state:
case cons.inr
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
h : a ∈ l0.toList
⊢ a ∈ l₂

Tactic:
exact mem_of_subset' s h

Result:
no goals

Proof state:
α : Type u_1
a : Lists α
b✝ : Bool
a0 : Lists' α b✝
l0 l₂ : Lists' α true
s : a0.cons' l0 ⊆ l₂
h : a ∈ (a0.cons' l0).toList
⊢ a ∈ l₂

Tactic:
obtain - | ⟨e, m, s⟩ := s

Result:
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
h : a ∈ (a✝.snd.cons' l0).toList
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
⊢ a ∈ l₂
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (ho : ∀ i, IsOpen (U i))
    (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U

Proof state:
case refine_2
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : ∃ f, (∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)) ∧ f.IsSubordinate U
⊢ ∃ f, f.IsSubordinate U

Tactic:
rcases this with ⟨f, hf, hfU⟩

Result:
case refine_2.intro.intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
f : BumpCovering ι M s
hf : ∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)
hfU : f.IsSubordinate U
⊢ ∃ f, f.IsSubordinate U

Proof state:
case refine_1.intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hf : EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
exact ⟨f, f.contMDiff, hf⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
f : BumpCovering ι M s
hf : ∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)
hfU : f.IsSubordinate U
⊢ ∃ f, f.IsSubordinate U

Tactic:
exact ⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_eq_iff {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) (y : Ordinal) :
    log b x = y ↔ b ^ y ≤ x ∧ x < b ^ succ y

Proof state:
case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ succ y → log b x = y

Tactic:
rintro ⟨hx₁, hx₂⟩

Result:
case mpr.intro
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ succ y
⊢ log b x = y

Proof state:
case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ b ^ log b x ≤ x ∧ x < b ^ succ (log b x)

Tactic:
use opow_log_le_self b hx, lt_opow_succ_log_self hb x

Result:
no goals

Proof state:
case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y → b ^ y ≤ x ∧ x < b ^ succ y

Tactic:
rintro rfl

Result:
case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ b ^ log b x ≤ x ∧ x < b ^ succ (log b x)

Proof state:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y ↔ b ^ y ≤ x ∧ x < b ^ succ y

Tactic:
constructor

Result:
case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y → b ^ y ≤ x ∧ x < b ^ succ y

case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ succ y → log b x = y

Proof state:
case mpr.intro
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ succ y
⊢ log b x = y

Tactic:
apply le_antisymm

Result:
case mpr.intro.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ succ y
⊢ log b x ≤ y

case mpr.intro.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ succ y
⊢ y ≤ log b x

Proof state:
case mpr.intro.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ succ y
⊢ y ≤ log b x

Tactic:
rwa [← opow_le_iff_le_log hb hx]

Result:
no goals

Proof state:
case mpr.intro.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ succ y
⊢ log b x ≤ y

Tactic:
rwa [← lt_succ_iff, ← lt_opow_iff_log_lt hb hx]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_balanceL (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (balanceL l x r) = balanceR (dual r) x (dual l)

Proof state:
case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l x_2 r l_ih r_ih =>
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih =>
        rec nil
          (fun size_1 l x_2 r l_ih r_ih =>
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> try rfl

Result:
case pos.node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l x_2 r l_ih r_ih =>
              if size_1 < ratio * size then
                node (ls + rs + 1) (node lls lll llx llr) lx
                  (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        (node lls lll llx llr)).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih =>
        rec nil
          (fun size_1 l x_2 r l_ih r_ih =>
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x (node lrs lrl lrx lrr).dual) lx
                (node lls lll llx llr).dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx (node lls lll llx llr).dual))
          (node lrs lrl lrx lrr).dual)
      (node lls lll llx llr).dual
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpIndSMul_empty {x : G} : condExpIndSMul hm MeasurableSet.empty
    ((measure_empty (μ := μ)).le.trans_lt ENNReal.coe_lt_top).ne x = 0

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
x : G
⊢ condExpIndSMul hm ⋯ ⋯ x = 0

Tactic:
rw [condExpIndSMul, indicatorConstLp_empty]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
x : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) 0) = 0

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
x : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) 0) = 0

Tactic:
simp only [Submodule.coe_zero, ContinuousLinearMap.map_zero]

Result:
no goals
-- Mathlib/Data/Int/Associated.lean
theorem Int.natAbs_eq_iff_associated {a b : ℤ} : a.natAbs = b.natAbs ↔ Associated a b

Proof state:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Associated a b

Tactic:
refine Int.natAbs_eq_natAbs_iff.trans ?_

Result:
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b

Proof state:
case mp.inl
a : ℤ
⊢ Associated a a

Tactic:
rfl

Result:
no goals

Proof state:
a : ℤ
⊢ a = a * ↑1

Tactic:
simp

Result:
no goals

Proof state:
case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b

Tactic:
rintro ⟨u, rfl⟩

Result:
case mpr.intro
a : ℤ
u : ℤˣ
⊢ a = a * ↑u ∨ a = -(a * ↑u)

Proof state:
b : ℤ
⊢ -b * ↑(-1) = b

Tactic:
simp

Result:
no goals

Proof state:
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b

Tactic:
rintro (rfl | rfl)

Result:
case mp.inl
a : ℤ
⊢ Associated a a

case mp.inr
b : ℤ
⊢ Associated (-b) b

Proof state:
a : ℤ
⊢ a = -(a * ↑(-1))

Tactic:
simp

Result:
no goals

Proof state:
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b

Tactic:
constructor

Result:
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b

case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b

Proof state:
case mpr.intro
a : ℤ
u : ℤˣ
⊢ a = a * ↑u ∨ a = -(a * ↑u)

Tactic:
obtain rfl | rfl := Int.units_eq_one_or u

Result:
case mpr.intro.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)

case mpr.intro.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))

Proof state:
case mpr.intro.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))

Tactic:
exact Or.inr (by simp)

Result:
no goals

Proof state:
case mpr.intro.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)

Tactic:
exact Or.inl (by simp)

Result:
no goals

Proof state:
case mp.inr
b : ℤ
⊢ Associated (-b) b

Tactic:
exact ⟨-1, by simp⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.eq_one_of_isUnit (hm : Monic p) (hpu : IsUnit p) : p = 1

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1

Tactic:
have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
⊢ p = 1

Tactic:
obtain ⟨q, h⟩ := hpu.exists_right_inv

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p = 1

Tactic:
rw [h, natDegree_one, eq_comm, add_eq_zero] at this

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1

Tactic:
exact hm.natDegree_eq_zero_iff_eq_one.mp this.1

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
⊢ p = 1

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
⊢ p = 1
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_add_C_pow (c : R) (m : ℕ) :
    derivative ((X + C c) ^ m) = C (m : R) * (X + C c) ^ (m - 1)

Proof state:
R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ derivative ((X + C c) ^ m) = C ↑m * (X + C c) ^ (m - 1)

Tactic:
rw [derivative_pow, derivative_X_add_C, mul_one]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem dist_circumcenter_sq_eq_sq_sub_circumradius {n : ℕ} {r : ℝ} (s : Simplex ℝ P n) {p₁ : P}
    (h₁ : ∀ i : Fin (n + 1), dist (s.points i) p₁ = r)
    (h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter)
    (h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)) :
    dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius

Tactic:
rw [dist_comm, ← h₁ 0,
  s.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₁ h]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) * dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) +
        dist p₁ ↑(s.orthogonalProjectionSpan p₁) * dist p₁ ↑(s.orthogonalProjectionSpan p₁) -
      s.circumradius * s.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) * dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) +
        dist p₁ ↑(s.orthogonalProjectionSpan p₁) * dist p₁ ↑(s.orthogonalProjectionSpan p₁) -
      s.circumradius * s.circumradius

Tactic:
simp only [h₁', dist_comm p₁, add_sub_cancel_left, Simplex.dist_circumcenter_eq_circumradius]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem inv_prodComparison_map_fst [IsIso (prodComparison F A B)] :
    inv (prodComparison F A B) ≫ F.map prod.fst = prod.fst

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map prod.fst = prod.fst

Tactic:
simp [IsIso.inv_comp_eq]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_ofFn :
    ∀ {n} {f : Fin n → α → σ}, (∀ i, Primrec (f i)) → Primrec fun a => List.ofFn fun i => f i a
  | 0, _, _ => by simp only [List.ofFn_zero]; exact const []
  | n + 1, f, hf => by
    simpa [List.ofFn_succ] using list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a => List.ofFn fun i => f i a

Tactic:
simpa [List.ofFn_succ] using list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Primrec (x✝¹ i)
⊢ Primrec fun a => List.ofFn fun i => x✝¹ i a

Tactic:
simp only [List.ofFn_zero]

Result:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Primrec (x✝¹ i)
⊢ Primrec fun a => []

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Primrec (x✝¹ i)
⊢ Primrec fun a => []

Tactic:
exact const []

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma strictAnti_rpow_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b < 1) :
    StrictAnti (b ^ · : ℝ → ℝ)

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x => rexp (log b * x)

Tactic:
exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
    <| Real.log_neg hb₀ hb₁

Result:
no goals

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x => b ^ x

Tactic:
simp_rw [Real.rpow_def_of_pos hb₀]

Result:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x => rexp (log b * x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_swapAt! (a : Array α) (i : Nat) (v : α) :
    (a.swapAt! i v).2.size = a.size

Proof state:
case isFalse
α : Type u_1
a : Array α
i : Nat
v : α
h✝ : ¬i < a.size
⊢ (panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swapAt!" 275 4
          ("index " ++ toString i ++ " out of bounds")).snd.size =
    a.size

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
⊢ (a.swapAt! i v).snd.size = a.size

Tactic:
simp only [swapAt!]

Result:
α : Type u_1
a : Array α
i : Nat
v : α
⊢ (if h : i < a.size then a.swapAt i v ⋯
        else
          panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swapAt!" 275 4
            ("index " ++ toString i ++ " out of bounds")).snd.size =
    a.size

Proof state:
case isTrue
α : Type u_1
a : Array α
i : Nat
v : α
h✝ : i < a.size
⊢ (a.swapAt i v ⋯).snd.size = a.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
⊢ (if h : i < a.size then a.swapAt i v ⋯
        else
          panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swapAt!" 275 4
            ("index " ++ toString i ++ " out of bounds")).snd.size =
    a.size

Tactic:
split

Result:
case isTrue
α : Type u_1
a : Array α
i : Nat
v : α
h✝ : i < a.size
⊢ (a.swapAt i v ⋯).snd.size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
v : α
h✝ : ¬i < a.size
⊢ (panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swapAt!" 275 4
          ("index " ++ toString i ++ " out of bounds")).snd.size =
    a.size
-- Mathlib/Data/Complex/Trigonometric.lean
theorem norm_exp_eq_iff_re_eq {x y : ℂ} : ‖exp x‖ = ‖exp y‖ ↔ x.re = y.re

Proof state:
x y : ℂ
⊢ ‖cexp x‖ = ‖cexp y‖ ↔ x.re = y.re

Tactic:
rw [norm_exp, norm_exp, Real.exp_eq_exp]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_norm_pow_id {n : ℕ} (h : 1 < n) :
    (fun x : E' => ‖x‖ ^ n) =o[𝓝 0] fun x => x

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ 1
⊢ (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x

Tactic:
simp only [pow_one] at this

Result:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖
⊢ (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖
⊢ (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x

Tactic:
exact isLittleO_norm_right.mp this

Result:
no goals

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
⊢ (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x

Tactic:
have := @isLittleO_norm_pow_norm_pow E' _ _ _ h

Result:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ 1
⊢ (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x