harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/KrullDimension.lean
/--
In a maximally long series, i.e one as long as the coheight of the first element, the coheight of
each element is its reverse index in the series.
-/
lemma coheight_eq_index_of_length_eq_head_coheight {p : LTSeries α} (h : p.length = coheight p.head)
    (i : Fin (p.length + 1)) : coheight (p i) = i.rev

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = coheight (RelSeries.head p)
i : Fin (p.length + 1)
⊢ coheight (p.toFun i) = ↑↑i.rev

Tactic:
simpa using height_eq_index_of_length_eq_height_last (α := αᵒᵈ) (p := p.reverse) (by simpa) i.rev

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = coheight (RelSeries.head p)
i : Fin (p.length + 1)
⊢ ↑(RelSeries.reverse p).length = height (RelSeries.reverse p).last

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem toSpanSingleton_smul' {α} [Monoid α] [DistribMulAction α M₁] [ContinuousConstSMul α M₁]
    [SMulCommClass R₁ α M₁] (c : α) (x : M₁) :
    toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x

Proof state:
case h
R₁ : Type u_1
inst✝⁹ : Semiring R₁
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₁
α : Type u_10
inst✝³ : Monoid α
inst✝² : DistribMulAction α M₁
inst✝¹ : ContinuousConstSMul α M₁
inst✝ : SMulCommClass R₁ α M₁
c : α
x : M₁
⊢ (toSpanSingleton R₁ (c • x)) 1 = (c • toSpanSingleton R₁ x) 1

Tactic:
rw [toSpanSingleton_apply, smul_apply, toSpanSingleton_apply, smul_comm]

Result:
no goals

Proof state:
R₁ : Type u_1
inst✝⁹ : Semiring R₁
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₁
α : Type u_10
inst✝³ : Monoid α
inst✝² : DistribMulAction α M₁
inst✝¹ : ContinuousConstSMul α M₁
inst✝ : SMulCommClass R₁ α M₁
c : α
x : M₁
⊢ toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x

Tactic:
ext1

Result:
case h
R₁ : Type u_1
inst✝⁹ : Semiring R₁
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₁
α : Type u_10
inst✝³ : Monoid α
inst✝² : DistribMulAction α M₁
inst✝¹ : ContinuousConstSMul α M₁
inst✝ : SMulCommClass R₁ α M₁
c : α
x : M₁
⊢ (toSpanSingleton R₁ (c • x)) 1 = (c • toSpanSingleton R₁ x) 1
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem tprod_inv : ∏' b, (f b)⁻¹ = (∏' b, f b)⁻¹

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
inst✝ : T2Space α
hf : ¬Multipliable f
⊢ ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹

Tactic:
simp [tprod_eq_one_of_not_multipliable hf,
  tprod_eq_one_of_not_multipliable (mt Multipliable.of_inv hf)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
inst✝ : T2Space α
⊢ ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹

Tactic:
by_cases hf : Multipliable f

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
inst✝ : T2Space α
hf : Multipliable f
⊢ ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹

case neg
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
inst✝ : T2Space α
hf : ¬Multipliable f
⊢ ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
inst✝ : T2Space α
hf : Multipliable f
⊢ ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹

Tactic:
exact hf.hasProd.inv.tprod_eq

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem prod_div_divisors {α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α) :
    (∏ d ∈ n.divisors, f (n / d)) = n.divisors.prod f

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
by_cases hn : n = 0

Result:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Proof state:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

Tactic:
exact prod_congr (image_div_divisors_eq_divisors n) (by simp)

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ n.divisors
y : ℕ
hy : y ∈ n.divisors
h : n / x = n / y
⊢ x = y

Tactic:
rw [mem_divisors] at hx hy

Result:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y

Proof state:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
rw [← prod_image]

Result:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, ∀ y ∈ n.divisors, n / x = n / y → x = y

Proof state:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, ∀ y ∈ n.divisors, n / x = n / y → x = y

Tactic:
intro x hx y hy h

Result:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ n.divisors
y : ℕ
hy : y ∈ n.divisors
h : n / x = n / y
⊢ x = y

Proof state:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y

Tactic:
exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, f x = f x

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_eq_nil (n : ℕ) : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Proof state:
case mpr.inl

⊢ primeFactorsList 0 = []

Tactic:
exact primeFactorsList_zero

Result:
no goals

Proof state:
case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1

Tactic:
exact Or.inr rfl

Result:
no goals

Proof state:
case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []

Tactic:
rcases h with (rfl | rfl)

Result:
case mpr.inl

⊢ primeFactorsList 0 = []

case mpr.inr

⊢ primeFactorsList 1 = []

Proof state:
case mp.succ.succ
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
injection h

Result:
no goals

Proof state:
case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
rw [primeFactorsList] at h

Result:
case mp.succ.succ
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Proof state:
case mp.zero
h : primeFactorsList 0 = []
⊢ 0 = 0 ∨ 0 = 1

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1

case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []

Proof state:
case mp
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1

Tactic:
rcases n with (_ | _ | n)

Result:
case mp.zero
h : primeFactorsList 0 = []
⊢ 0 = 0 ∨ 0 = 1

case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1

case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Proof state:
case mpr.inr

⊢ primeFactorsList 1 = []

Tactic:
exact primeFactorsList_one

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma isoSpec_hom_appTop :
    hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
have := congr(inv $hU.isoSpec_inv_appTop)

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
this : inv (Scheme.Hom.appTop hU.isoSpec.inv) = inv (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv)
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
this✝ : inv (Scheme.Hom.appTop hU.isoSpec.inv) = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
this : Scheme.Γ.map (inv hU.isoSpec.inv.op) = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
rwa [← op_inv, IsIso.Iso.inv_inv] at this

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
this : inv (Scheme.Hom.appTop hU.isoSpec.inv) = inv (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv)
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
rw [IsIso.inv_comp, IsIso.Iso.inv_inv, IsIso.Iso.inv_hom] at this

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
this : inv (Scheme.Hom.appTop hU.isoSpec.inv) = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
this : inv (Scheme.Hom.appTop hU.isoSpec.inv) = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
have := (Scheme.Γ.map_inv hU.isoSpec.inv.op).trans this

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
this✝ : inv (Scheme.Hom.appTop hU.isoSpec.inv) = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
this : Scheme.Γ.map (inv hU.isoSpec.inv.op) = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
⊢ Scheme.Hom.appTop hU.isoSpec.hom = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_some_eq_eq {t : RBNode α} : x ∈ t.find? cut → cut x = .eq

Proof state:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    cut x = Ordering.eq

Tactic:
split <;> try assumption

Result:
case node.h_3
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → cut x = Ordering.eq

Proof state:
case node.h_3
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → cut x = Ordering.eq

Tactic:
intro | rfl => assumption

Result:
no goals

Proof state:
case node.h_2
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ find? cut r✝ = some x → cut x = Ordering.eq

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
x : α
t : RBNode α
⊢ x ∈ find? cut t → cut x = Ordering.eq

Tactic:
induction t <;> simp [find?]

Result:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    cut x = Ordering.eq

Proof state:
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝¹ : Ordering
heq✝ : cut v✝ = Ordering.eq
x✝ : some v✝ = some x
l_ih✝ : v✝ ∈ find? cut l✝ → cut v✝ = Ordering.eq
r_ih✝ : v✝ ∈ find? cut r✝ → cut v✝ = Ordering.eq
⊢ cut v✝ = Ordering.eq

Tactic:
assumption

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesAt.prod {e : E} {f : E → F} {g : E → G}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesAt f p e) (hg : HasFPowerSeriesAt g q e) :
    HasFPowerSeriesAt (fun x ↦ (f x, g x)) (p.prod q) e

Proof state:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w✝¹ : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w✝¹
w✝ : ℝ≥0∞
hg : HasFPowerSeriesOnBall g q e w✝
⊢ HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e

Tactic:
exact ⟨_, hf.prod hg⟩

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesAt f p e
hg : HasFPowerSeriesAt g q e
⊢ HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e

Tactic:
rcases hf with ⟨_, hf⟩

Result:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g q e
w✝ : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w✝
⊢ HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e

Proof state:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g q e
w✝ : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w✝
⊢ HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e

Tactic:
rcases hg with ⟨_, hg⟩

Result:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w✝¹ : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w✝¹
w✝ : ℝ≥0∞
hg : HasFPowerSeriesOnBall g q e w✝
⊢ HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem le_exp_log (x : ℝ) : x ≤ exp (log x)

Proof state:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
rw [exp_log_eq_abs h_zero]

Result:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|

Proof state:
case pos
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)

Tactic:
rw [h_zero, log, dif_pos rfl, exp_zero]

Result:
case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1

Proof state:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|

Tactic:
exact le_abs_self _

Result:
no goals

Proof state:
x : ℝ
⊢ x ≤ rexp (log x)

Tactic:
by_cases h_zero : x = 0

Result:
case pos
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)

case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Proof state:
case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@[simp]
lemma evaluation_eq_zero_iff_not_mem_basicOpen (x : U) (f : X.presheaf.obj (op U)) :
    X.evaluation x f = 0 ↔ x.val ∉ X.toRingedSpace.basicOpen f

Proof state:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ ¬(ConcreteCategory.hom (X.evaluation x)) f = 0 ↔
    IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U ↑x ⋯)) f)

Tactic:
exact (IsLocalRing.residue_ne_zero_iff_isUnit _)

Result:
no goals

Proof state:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f

Tactic:
rw [X.toRingedSpace.mem_basicOpen f x.1 x.2, ← not_iff_not, not_not]

Result:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ ¬(ConcreteCategory.hom (X.evaluation x)) f = 0 ↔
    IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U ↑x ⋯)) f)
-- Mathlib/CategoryTheory/Sites/CoversTop.lean
lemma familyOfElements_isCompatible (hx : x.IsCompatible) (X : C) :
    (familyOfElements x X).Compatible

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X : C
⊢ (x.familyOfElements X).Compatible

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ ⟨i₁, ⟨φ₁⟩⟩ ⟨i₂, ⟨φ₂⟩⟩ _

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
a✝ : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁.op (x.familyOfElements X f₁ ⋯) = F.map g₂.op (x.familyOfElements X f₂ ⋯)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
a✝ : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁.op (x.familyOfElements X f₁ ⋯) = F.map g₂.op (x.familyOfElements X f₂ ⋯)

Tactic:
simpa [hx.familyOfElements_apply f₁ i₁ φ₁,
  hx.familyOfElements_apply f₂ i₂ φ₂] using hx Z i₁ i₂ (g₁ ≫ φ₁) (g₂ ≫ φ₂)

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_inf_mul_relfinrank_of_le (h : A ≤ B) :
    A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ≤ B
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank_of_le C h))

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_rpow_of_exponent_neg {x y z : ℝ} (hy : 0 < y) (hxy : y < x) (hz : z < 0) :
    x ^ z < y ^ z

Proof state:
x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ 0 ≤ y

Tactic:
positivity

Result:
no goals

Proof state:
x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ x ^ z < y ^ z

Tactic:
rw [← neg_neg z, Real.rpow_neg (le_of_lt hx) (-z), Real.rpow_neg (le_of_lt hy) (-z),
    inv_lt_inv₀ (rpow_pos_of_pos hx _) (rpow_pos_of_pos hy _)]

Result:
x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ y ^ (-z) < x ^ (-z)

Proof state:
x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ y ^ (-z) < x ^ (-z)

Tactic:
exact Real.rpow_lt_rpow (by positivity) hxy <| neg_pos_of_neg hz

Result:
no goals

Proof state:
x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
⊢ x ^ z < y ^ z

Tactic:
have hx : 0 < x := hy.trans hxy

Result:
x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ x ^ z < y ^ z
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem filterMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Option β)) :
    l.toArray.filterMapM f = toArray <$> l.filterMapM f

Proof state:
case cons.e_a.h.none
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
⊢ (do
      let init ←
        match none with
          | some b => pure (acc.reverse ++ [b]).toArray
          | none => pure acc.reverse.toArray
      List.foldlM
          (fun x y => do
            let __do_lift ← f y
            match __do_lift with
              | some b => pure (x.push b)
              | none => pure x)
          init xs) =
    toArray <$>
      match none with
      | none => filterMapM.loop f xs acc
      | some b => filterMapM.loop f xs (b :: acc)

Tactic:
simp only [pure_bind]

Result:
case cons.e_a.h.none
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      acc.reverse.toArray xs =
    toArray <$> filterMapM.loop f xs acc
-- Mathlib/Algebra/GradedMonoid.lean
theorem GradedMonoid.list_prod_map_eq_dProd (l : List α) (f : α → GradedMonoid A) :
    (l.map f).prod = GradedMonoid.mk _ (l.dProd (fun i => (f i).1) fun i => (f i).2)

Proof state:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = mk (l.dProdIndex fun i => (f i).fst) (l.dProd (fun i => (f i).fst) fun i => (f i).snd)

Tactic:
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]

Result:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = (List.map (fun a => ⟨(f a).fst, (f a).snd⟩) l).prod

Proof state:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = (List.map (fun a => ⟨(f a).fst, (f a).snd⟩) l).prod

Tactic:
simp_rw [Sigma.eta]

Result:
no goals