harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem rename_eval₂ (g : τ → MvPolynomial σ R) :
    rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (rename k ∘ g)

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p * X n))

Tactic:
intros

Result:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : (rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p✝)
⊢ (rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p✝ * X n✝))

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : (rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p✝)
⊢ (rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p✝ * X n✝))

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_eq_iff_natDegree_eq {p : R[X]} {n : ℕ} (hp : p ≠ 0) :
    p.degree = n ↔ p.natDegree = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
rw [degree_eq_natDegree hp]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑p.natDegree = ↑n ↔ p.natDegree = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑p.natDegree = ↑n ↔ p.natDegree = n

Tactic:
exact WithBot.coe_eq_coe

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_mul_of_domain {R : Type*} [Ring R] [NoZeroDivisors R] (f g : R[X]) :
    reverse (f * g) = reverse f * reverse g

Proof state:
case pos
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
simp only [f0, zero_mul, reverse_zero]

Result:
no goals

Proof state:
case neg
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : ¬g = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
simp [reverse_mul, *]

Result:
no goals

Proof state:
case pos
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
rw [g0, mul_zero, reverse_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by_cases f0 : f = 0

Result:
case pos
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

case neg
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Proof state:
case neg
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by_cases g0 : g = 0

Result:
case pos
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ (f * g).reverse = f.reverse * g.reverse

case neg
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : ¬g = 0
⊢ (f * g).reverse = f.reverse * g.reverse
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem Algebra.IsIntegral.tower_top [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    [h : Algebra.IsIntegral R T] : Algebra.IsIntegral S T where
  isIntegral

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ∀ (x : T), IsIntegral S x

Tactic:
apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)

Result:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ((algebraMap S T).comp (algebraMap R S)).IsIntegral

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral

Tactic:
exact h.isIntegral

Result:
no goals

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ((algebraMap S T).comp (algebraMap R S)).IsIntegral

Tactic:
rw [← IsScalarTower.algebraMap_eq R S T]

Result:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral
-- Mathlib/Topology/Algebra/Support.lean
theorem LocallyFinite.smul_right [Zero M] [SMulZeroClass R M]
    {f : ι → X → M} (h : LocallyFinite fun i ↦ support <| f i) (s : ι → X → R) :
    LocallyFinite fun i ↦ support <| s i • f i :=
  h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, smul_zero]

Proof state:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝² : TopologicalSpace X
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : ι → X → M
h✝ : LocallyFinite fun i => support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ (s i • f i) x = 0

Tactic:
rw [Pi.smul_apply', h, smul_zero]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem subsingleton_iff : Subsingleton (LieSubmodule R L M) ↔ Subsingleton M :=
  have h : Subsingleton (LieSubmodule R L M) ↔ Subsingleton (Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
⊢ Subsingleton (LieSubmodule R L M) ↔ Subsingleton (Submodule R M)

Tactic:
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toSubmodule_inj,
  top_toSubmodule, bot_toSubmodule]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem incidenceSet_inter_incidenceSet_of_not_adj (h : ¬G.Adj a b) (hn : a ≠ b) :
    G.incidenceSet a ∩ G.incidenceSet b = ∅

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
u : Sym2 V
ha : u ∈ G.incidenceSet a
hb : u ∈ G.incidenceSet b
⊢ False

Tactic:
exact h (G.adj_of_mem_incidenceSet hn ha hb)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅

Tactic:
simp_rw [Set.eq_empty_iff_forall_not_mem, Set.mem_inter_iff, not_and]

Result:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ ∀ x ∈ G.incidenceSet a, x ∉ G.incidenceSet b

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ ∀ x ∈ G.incidenceSet a, x ∉ G.incidenceSet b

Tactic:
intro u ha hb

Result:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
u : Sym2 V
ha : u ∈ G.incidenceSet a
hb : u ∈ G.incidenceSet b
⊢ False
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
lemma toNNReal_add_add_neg_add_neg_eq (f g : C(X, ℝ)) :
    (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal =
      (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

Proof state:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ ↑(((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) x) = ↑(((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) x)

Tactic:
simp [max_neg_zero, -neg_add_rev]

Result:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ (f x + g x) ⊔ 0 + (-f x + f x ⊔ 0) + (-g x + g x ⊔ 0) = -(f x + g x) + (f x + g x) ⊔ 0 + f x ⊔ 0 + g x ⊔ 0

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
⊢ (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

Tactic:
ext x

Result:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ ↑(((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) x) = ↑(((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) x)

Proof state:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ (f x + g x) ⊔ 0 + (-f x + f x ⊔ 0) + (-g x + g x ⊔ 0) = -(f x + g x) + (f x + g x) ⊔ 0 + f x ⊔ 0 + g x ⊔ 0

Tactic:
abel

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_nhds (hff' : ∀ᶠ x in 𝓝 a, HasDerivAt f (f' x) x)
    (hgg' : ∀ᶠ x in 𝓝 a, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in 𝓝 a, g' x ≠ 0)
    (hfa : Tendsto f (𝓝 a) (𝓝 0)) (hga : Tendsto g (𝓝 a) (𝓝 0))
    (hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l) : Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Proof state:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Tactic:
apply @lhopital_zero_nhds' _ _ _ f' _ g' <;>
  (first | apply eventually_nhdsWithin_of_eventually_nhds |
    apply tendsto_nhdsWithin_of_tendsto_nhds) <;> assumption

Result:
no goals

Proof state:
case hg'
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Result:
case hg'.h
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0

Proof state:
case hdiv
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun x => f' x / g' x) (𝓝[≠] a) l

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
 apply tendsto_nhdsWithin_of_tendsto_nhds

Result:
case hdiv.h
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun x => f' x / g' x) (𝓝 a) l

Proof state:
case hdiv
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun x => f' x / g' x) (𝓝[≠] a) l

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Result:
case hdiv.h
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun x => f' x / g' x) (𝓝 a) l
-- Mathlib/Data/Multiset/Nodup.lean
theorem nodup_iff_count_le_one [DecidableEq α] {s : Multiset α} : Nodup s ↔ ∀ a, count a s ≤ 1 :=
  Quot.induction_on s fun _l => by
    simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
    exact List.nodup_iff_count_le_one

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1

Tactic:
exact List.nodup_iff_count_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔ ∀ (a : α), count a (Quot.mk (⇑(isSetoid α)) _l) ≤ 1

Tactic:
simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem isNormal_veblen_zero : IsNormal (veblen · 0) :=
  (isNormal_opow one_lt_omega0).veblenWith_zero (by simp)

Proof state:
⊢ 0 < ω ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_union {x y z : ZFSet.{u}} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

Proof state:
x y z : ZFSet.{u}
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

Tactic:
rw [← mem_toSet]

Result:
x y z : ZFSet.{u}
⊢ z ∈ (x ∪ y).toSet ↔ z ∈ x ∨ z ∈ y

Proof state:
x y z : ZFSet.{u}
⊢ z ∈ (x ∪ y).toSet ↔ z ∈ x ∨ z ∈ y

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
@[reassoc (attr := simp)]
lemma germ_stalkPullbackHom
    (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) (U : Opens Y) (hU : f x ∈ U) :
    F.germ U (f x) hU ≫ stalkPullbackHom C f F x =
      ((pushforwardPullbackAdjunction C f).unit.app F).app _ ≫
        ((pullback C f).obj F).germ ((Opens.map f).obj U) x hU

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ U ((ConcreteCategory.hom f) x) hU ≫ stalkPullbackHom C f F x =
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op U) ≫ ((pullback C f).obj F).germ ((Opens.map f).obj U) x hU

Tactic:
simp [stalkPullbackHom, germ, stalkFunctor, stalkPushforward]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_swap : (μ.prod ν).map Prod.swap = ν.prod μ

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (μ.prod ν).map Prod.swap = ν.prod μ

Tactic:
apply Subtype.ext

Result:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ ↑((μ.prod ν).map Prod.swap) = ↑(ν.prod μ)

Proof state:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ ↑((μ.prod ν).map Prod.swap) = ↑(ν.prod μ)

Tactic:
simp [Measure.prod_swap]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_pow₀ (ha : 1 ≤ a) : ∀ {n : ℕ}, 1 ≤ a ^ n
  | 0 => by rw [pow_zero]
  | n + 1 => by
    simpa only [pow_succ', mul_one]
      using mul_le_mul ha (one_le_pow₀ ha) zero_le_one (zero_le_one.trans ha)

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
n : ℕ
⊢ 1 ≤ a ^ (n + 1)

Tactic:
simpa only [pow_succ', mul_one]
  using mul_le_mul ha (one_le_pow₀ ha) zero_le_one (zero_le_one.trans ha)

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
⊢ 1 ≤ a ^ 0

Tactic:
rw [pow_zero]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_lt_iff_not_dvd {k : ℕ} :
    emultiplicity a b < k ↔ ¬a ^ k ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ ¬a ^ k ∣ b

Tactic:
rw [pow_dvd_iff_le_emultiplicity, not_le]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
⊢ map f (dirac a) = dirac (f a)

Tactic:
exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
⊢ map f (dirac a) = dirac (f a)

Tactic:
classical
exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (map f (dirac a)) s = (dirac (f a)) s

Tactic:
simp [hs, map_apply hf hs, hf hs, indicator_apply]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBase.closure_eq (hB : M.IsBase B) : M.closure B = M.E

Proof state:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.closure B = M.E

Tactic:
rw [← isBasis_ground_iff] at hB

Result:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E

Proof state:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E

Tactic:
rw [hB.closure_eq_closure, closure_ground]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_midpoint_right (p₁ p₂ p₃ : P) : ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ¬p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_right

Result:
no goals

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
simp [h]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
by_cases h : p₃ = p₂

Result:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ¬p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
-- Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean
theorem closedUnderLimitsOfShape_walkingParallelPair_isIndObject [HasEqualizers C] :
    ClosedUnderLimitsOfShape WalkingParallelPair (IsIndObject (C := C))

Proof state:
case h.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
hF : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
P : IndParallelPairPresentation (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)
⊢ IsIndObject (limit F)

Tactic:
exact IsIndObject.map
  (HasLimit.isoOfNatIso (P.parallelPairIsoParallelPairCompYoneda.symm ≪≫
    (diagramIsoParallelPair _).symm)).hom
  (isIndObject_limit_comp_yoneda_comp_colim (parallelPair P.φ P.ψ)
    (fun i => isIndObject_limit_comp_yoneda _))

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
⊢ ∀ {F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v} [inst : HasLimit F],
    (∀ (j : WalkingParallelPair), IsIndObject (F.obj j)) → IsIndObject (limit F)

Tactic:
intro F hF h

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
hF : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
⊢ IsIndObject (limit F)

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
hF : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
⊢ IsIndObject (limit F)

Tactic:
obtain ⟨P⟩ := nonempty_indParallelPairPresentation (h WalkingParallelPair.zero)
  (h WalkingParallelPair.one) (F.map WalkingParallelPairHom.left)
  (F.map WalkingParallelPairHom.right)

Result:
case h.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
hF : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
P : IndParallelPairPresentation (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)
⊢ IsIndObject (limit F)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
⊢ ClosedUnderLimitsOfShape WalkingParallelPair IsIndObject

Tactic:
apply closedUnderLimitsOfShape_of_limit

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasEqualizers C
⊢ ∀ {F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v} [inst : HasLimit F],
    (∀ (j : WalkingParallelPair), IsIndObject (F.obj j)) → IsIndObject (limit F)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem eqToHom_comp_d {i i' j : ι} (rij : c.Rel i j) (rij' : c.Rel i' j) :
    eqToHom (congr_arg C.X (c.prev_eq rij rij')) ≫ C.d i' j = C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i i' j : ι
rij : c.Rel i j
rij' : c.Rel i' j
⊢ eqToHom ⋯ ≫ C.d i' j = C.d i j

Tactic:
obtain rfl := c.prev_eq rij rij'

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : c.Rel i j
⊢ eqToHom ⋯ ≫ C.d i j = C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : c.Rel i j
⊢ eqToHom ⋯ ≫ C.d i j = C.d i j

Tactic:
simp only [eqToHom_refl, id_comp]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.one_smul_sub_smul_one_mem_ideal (a : S) :
    (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ KaehlerDifferential.ideal R S

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : S
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ ideal R S

Tactic:
simp [RingHom.mem_ker]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@[simp] lemma add_apply {f g : E →WOT[𝕜] F} (x : E) : (f + g) x = f x + g x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f g : E →WOT[𝕜] F
x : E
⊢ (f + g) x = f x + g x

Tactic:
simp only [DFunLike.coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f g : E →WOT[𝕜] F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (f + g))).toFun x =
    (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x +
      (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm g)).toFun x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f g : E →WOT[𝕜] F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (f + g))).toFun x =
    (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x +
      (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm g)).toFun x

Tactic:
rfl

Result:
no goals