harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem tprodCoeff_eq_smul_tprod (z : R) (f : Π i, s i) : tprodCoeff R z f = z • tprod R f

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R (z • 1) f = z • (tprod R) f

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
⊢ z = z • 1

Tactic:
simp only [mul_one, Algebra.id.smul_eq_mul]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
⊢ tprodCoeff R z f = z • (tprod R) f

Tactic:
have : z = z • (1 : R) := by simp only [mul_one, Algebra.id.smul_eq_mul]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R z f = z • (tprod R) f

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R z f = z • (tprod R) f

Tactic:
conv_lhs => rw [this]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R (z • 1) f = z • (tprod R) f
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
lemma epi_iff_mk_eq_top [Balanced C] (f : X ⟶ Y) [Mono f] :
    Epi f ↔ Subobject.mk f = ⊤

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : Balanced C
f : X ⟶ Y
inst✝ : Mono f
⊢ Epi f ↔ IsIso f

Tactic:
exact ⟨fun _ ↦ isIso_of_mono_of_epi f, fun _ ↦ inferInstance⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : Balanced C
f : X ⟶ Y
inst✝ : Mono f
⊢ Epi f ↔ mk f = ⊤

Tactic:
rw [← isIso_iff_mk_eq_top]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : Balanced C
f : X ⟶ Y
inst✝ : Mono f
⊢ Epi f ↔ IsIso f
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem perpBisector_eq_top : perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ ∈ ⊤

Tactic:
trivial

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
p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ = p₂

Tactic:
rw [← left_mem_perpBisector, h]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ ∈ ⊤

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂

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

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ = p₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_cons (ctx : Context) (k : Nat) (v : Var) (p : Poly) : denote ctx ((k, v) :: p) = k * v.denote ctx + p.denote ctx

Proof state:
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx ((k, v) :: p) = k * Var.denote ctx v + denote ctx p

Tactic:
match p with
| []     => simp
| _ :: m => simp [denote_cons]

Result:
no goals

Proof state:
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx [(k, v)] = k * Var.denote ctx v + denote ctx []

Tactic:
simp

Result:
no goals

Proof state:
ctx : Context
k : Nat
v : Var
p : Poly
head✝ : Nat × Var
m : List (Nat × Var)
⊢ denote ctx ((k, v) :: head✝ :: m) = k * Var.denote ctx v + denote ctx (head✝ :: m)

Tactic:
simp [denote_cons]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
lemma analyticAt_cuspFunction_zero [NeZero n] [ModularFormClass F Γ(n) k] :
    AnalyticAt ℂ (cuspFunction n f) 0 :=
  DifferentiableOn.analyticAt
    (fun q hq ↦ (differentiableAt_cuspFunction _ _ hq).differentiableWithinAt)
    (by simpa only [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one)

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
⊢ (fun q => Real.lt✝ ‖q‖ 1) ∈ nhds 0

Tactic:
simpa only [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem toList_head? {i j} (w : NeWord M i j) : w.toList.head? = Option.some ⟨i, w.head⟩

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ w.toList.head? = some ⟨i, w.head⟩

Tactic:
rw [← Option.mem_def]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨i, w.head⟩ ∈ w.toList.head?

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨i✝, _w₁✝.head⟩ ∈ _w₁✝.toList.head?
_w₂_ih✝ : ⟨k✝, _w₂✝.head⟩ ∈ _w₂✝.toList.head?
⊢ ⟨i✝, (_w₁✝.append _hne✝ _w₂✝).head⟩ ∈ _w₁✝.toList.head?

Tactic:
assumption

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨i, w.head⟩ ∈ w.toList.head?

Tactic:
induction w

Result:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).head⟩ ∈ (singleton x✝ a✝).toList.head?

case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨i✝, _w₁✝.head⟩ ∈ _w₁✝.toList.head?
_w₂_ih✝ : ⟨k✝, _w₂✝.head⟩ ∈ _w₂✝.toList.head?
⊢ ⟨i✝, (_w₁✝.append _hne✝ _w₂✝).head⟩ ∈ (_w₁✝.append _hne✝ _w₂✝).toList.head?

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨i✝, _w₁✝.head⟩ ∈ _w₁✝.toList.head?
_w₂_ih✝ : ⟨k✝, _w₂✝.head⟩ ∈ _w₂✝.toList.head?
⊢ ⟨i✝, (_w₁✝.append _hne✝ _w₂✝).head⟩ ∈ (_w₁✝.append _hne✝ _w₂✝).toList.head?

Tactic:
exact List.mem_head?_append_of_mem_head? (by assumption)

Result:
no goals

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.head? = some ⟨i✝, (singleton x✝ a✝).head⟩

Tactic:
rfl

Result:
no goals

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).head⟩ ∈ (singleton x✝ a✝).toList.head?

Tactic:
rw [Option.mem_def]

Result:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.head? = some ⟨i✝, (singleton x✝ a✝).head⟩
-- Mathlib/Data/Finmap.lean
lemma nodup_keys {m : Multiset (Σ a, β a)} : m.keys.Nodup ↔ m.NodupKeys

Proof state:
case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ (keys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)).Nodup ↔ NodupKeys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
⊢ m.keys.Nodup ↔ m.NodupKeys

Tactic:
rcases m with ⟨l⟩

Result:
case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ (keys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)).Nodup ↔ NodupKeys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)
-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
lemma IsClosedImmersion.of_comp [IsClosedImmersion (f ≫ g)] [IsSeparated g] :
    IsClosedImmersion f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion (f ≫ g)
inst✝ : IsSeparated g
⊢ IsClosedImmersion f

Tactic:
rw [← pullback.lift_snd (𝟙 _) f (Category.id_comp (f ≫ g))]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion (f ≫ g)
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.lift (𝟙 X) f ⋯ ≫ pullback.snd (f ≫ g) g)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion (f ≫ g)
inst✝ : IsSeparated g
this : IsClosedImmersion (pullback.snd (f ≫ g) g)
⊢ IsClosedImmersion (pullback.lift (𝟙 X) f ⋯ ≫ pullback.snd (f ≫ g) g)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion (f ≫ g)
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.lift (𝟙 X) f ⋯ ≫ pullback.snd (f ≫ g) g)

Tactic:
have := MorphismProperty.pullback_snd (P := @IsClosedImmersion) (f ≫ g) g inferInstance

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion (f ≫ g)
inst✝ : IsSeparated g
this : IsClosedImmersion (pullback.snd (f ≫ g) g)
⊢ IsClosedImmersion (pullback.lift (𝟙 X) f ⋯ ≫ pullback.snd (f ≫ g) g)
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_mul (a b : MvPolynomial σ R) :
    (a * b).totalDegree ≤ a.totalDegree + b.totalDegree :=
  sup_support_mul_le (by exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a b : MvPolynomial σ R
⊢ ∀ {a b : σ →₀ ℕ}, ((a + b).sum fun x e => e) ≤ (a.sum fun x e => e) + b.sum fun x e => e

Tactic:
exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
/-- The characteristic equals the exponential characteristic iff the former is prime. -/
lemma char_eq_expChar_iff (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ p.Prime

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p

Tactic:
rcases hq with q | hq_prime

Result:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 1 ↔ Nat.Prime p

case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p

Proof state:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p

Tactic:
exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 1 ↔ Nat.Prime p

Tactic:
rw [(CharP.eq R hp inferInstance : p = 0)]

Result:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
theorem add_comp (f g : X ⟶ Y) (h : Y ⟶ Z) : (f + g) ≫ h = f ≫ h + g ≫ h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g ≫ h = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc (f ≫ h) (g ≫ h)

Tactic:
congr

Result:
case e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.desc f g ≫ h = biprod.desc (f ≫ h) (g ≫ h)

Proof state:
case e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.desc f g ≫ h = biprod.desc (f ≫ h) (g ≫ h)

Tactic:
ext <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
simp only [add_eq_right_addition, Category.assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g ≫ h = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc (f ≫ h) (g ≫ h)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_cons_iff {P : Vector α (n + 1) → Prop} :
    (∀ v : Vector α (n + 1), P v) ↔ (∀ (x : α) (v : Vector α n), P (v.push x))

Proof state:
case mp
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (v : Vector α (n + 1)), P v
x✝ : α
v✝ : Vector α n
⊢ P (v✝.push x✝)

Tactic:
apply h

Result:
no goals

Proof state:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
⊢ (∀ (x : α) (v : Vector α n), P (v.push x)) → ∀ (v : Vector α (n + 1)), P v

Tactic:
intro h v

Result:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
⊢ P v

Proof state:
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
⊢ (∀ (v : Vector α (n + 1)), P v) ↔ ∀ (x : α) (v : Vector α n), P (v.push x)

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
⊢ (∀ (v : Vector α (n + 1)), P v) → ∀ (x : α) (v : Vector α n), P (v.push x)

case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
⊢ (∀ (x : α) (v : Vector α n), P (v.push x)) → ∀ (v : Vector α (n + 1)), P v

Proof state:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
w : v = v.pop.push v.back
⊢ P (v.pop.push v.back)

Tactic:
apply h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
⊢ v = v.pop.push v.back

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
w : v = v.pop.push v.back
⊢ P v

Tactic:
rw [w]

Result:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
w : v = v.pop.push v.back
⊢ P (v.pop.push v.back)

Proof state:
case mp
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
⊢ (∀ (v : Vector α (n + 1)), P v) → ∀ (x : α) (v : Vector α n), P (v.push x)

Tactic:
intro h _ _

Result:
case mp
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (v : Vector α (n + 1)), P v
x✝ : α
v✝ : Vector α n
⊢ P (v✝.push x✝)

Proof state:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
⊢ P v

Tactic:
have w : v = v.pop.push v.back := by simp

Result:
case mpr
α : Type u_1
n : Nat
P : Vector α (n + 1) → Prop
h : ∀ (x : α) (v : Vector α n), P (v.push x)
v : Vector α (n + 1)
w : v = v.pop.push v.back
⊢ P v
-- Mathlib/RingTheory/KrullDimension/Basic.lean
lemma Ring.krullDimLE_one_iff_of_isPrime_bot [(⊥ : Ideal R).IsPrime] :
    Ring.KrullDimLE 1 R ↔ ∀ I : Ideal R, I ≠ ⊥ → I.IsPrime → I.IsMaximal

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := OrderBot.mk ⋯
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
  Order.krullDim_le_one_iff_forall_isMax, (PrimeSpectrum.equivSubtype R).forall_congr_left,
  Subtype.forall, PrimeSpectrum.isMax_iff, forall_comm (α := _ ≠ ⊥),
  ne_eq, PrimeSpectrum.ext_iff]

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := OrderBot.mk ⋯
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ¬((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal = ⊥.asIdeal →
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → ¬I = ⊥ → I.IsMaximal

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
letI : OrderBot (PrimeSpectrum R) := { bot := ⟨⊥, ‹_›⟩, bot_le I := bot_le (a := I.1) }

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := OrderBot.mk ⋯
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := OrderBot.mk ⋯
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ¬((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal = ⊥.asIdeal →
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → ¬I = ⊥ → I.IsMaximal

Tactic:
rfl

Result:
no goals
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem subtype_toEquiv_inclusion {f g : M ≃ₚ[L] N} (h : f ≤ g) :
    (subtype _).comp (g.toEquiv.toEmbedding.comp (Substructure.inclusion (dom_le_dom h))) =
      (subtype _).comp f.toEquiv.toEmbedding

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
w✝ : f.dom ≤ g.dom
eq : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
exact eq

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
let ⟨_, eq⟩ := h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
w✝ : f.dom ≤ g.dom
eq : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_left_on_Ioo (hab : a < b) (hdf : DifferentiableOn ℝ f (Ioo a b))
    (hg' : ∀ x ∈ Ioo a b, (deriv g) x ≠ 0) (hfb : Tendsto f (𝓝[<] b) (𝓝 0))
    (hgb : Tendsto g (𝓝[<] b) (𝓝 0))
    (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝[<] b) l) :
    Tendsto (fun x => f x / g x) (𝓝[<] b) l

Proof state:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] b) l

Tactic:
have hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx =>
  (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)

Result:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] b) l

Proof state:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] b) l

Tactic:
exact HasDerivAt.lhopital_zero_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
  (fun x hx => (hdg x hx).hasDerivAt) hg' hfb hgb hdiv

Result:
no goals

Proof state:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] b) l

Tactic:
have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
  by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)

Result:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] b) l
-- Mathlib/Algebra/Group/Pi/Units.lean
@[to_additive]
lemma IsUnit.val_inv_apply (hx : IsUnit x) (i : ι) : (hx.unit⁻¹).1 i = (hx.apply i).unit⁻¹

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹

Tactic:
rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i)⁻¹ = ↑⋯.unit⁻¹

Proof state:
case e_self.e_a
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ MulEquiv.piUnits hx.unit i = ⋯.unit

Tactic:
ext

Result:
case e_self.e_a.a
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i) = ↑⋯.unit

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i)⁻¹ = ↑⋯.unit⁻¹

Tactic:
congr

Result:
case e_self.e_a
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ MulEquiv.piUnits hx.unit i = ⋯.unit

Proof state:
case e_self.e_a.a
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i) = ↑⋯.unit

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem edist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
    edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄

Tactic:
simp only [edist_nndist]

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) ≤ ↑(nndist p₁ p₃) + ↑(nndist p₂ p₄)

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) ≤ ↑(nndist p₁ p₃) + ↑(nndist p₂ p₄)

Tactic:
norm_cast

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Tactic:
apply dist_vsub_vsub_le

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
/-- `2` is not a factor of an odd natural number. -/
lemma Odd.ne_two_of_dvd_nat {m n : ℕ} (hn : Odd n) (hm : m ∣ n) : m ≠ 2

Proof state:
m n : ℕ
hn : Odd n
hm : m ∣ n
⊢ m ≠ 2

Tactic:
rintro rfl

Result:
n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False

Proof state:
n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False

Tactic:
exact absurd (hn.of_dvd_nat hm) (by decide)

Result:
no goals

Proof state:
n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ ¬Odd 2

Tactic:
decide

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_Ici (f : α ≃o β) (a : α) : map f (Ici a) = Ici (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ici a) = Ici (f a)

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ici a)) ↔ x✝ ∈ ↑(Ici (f a))

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ici a)) ↔ x✝ ∈ ↑(Ici (f a))

Tactic:
simp

Result:
no goals