harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem toFunLinear_one_tmul_one :
    toFunLinear R A (1 ⊗ₜ[R] 1) = 1

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

Tactic:
rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_one : withTopEquiv 1 = 1

Proof state:
⊢ withTopEquiv 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Basic.lean
theorem isUnit_or_isUnit_of_isUnit_add {a b : R} (h : IsUnit (a + b)) : IsUnit a ∨ IsUnit b

Proof state:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu) <;> exact isUnit_of_mul_isUnit_right

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
a b : R
h : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
rcases h with ⟨u, hu⟩

Result:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u = a + b
⊢ IsUnit a ∨ IsUnit b

Proof state:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u = a + b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [← Units.inv_mul_eq_one, mul_add] at hu

Result:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit a ∨ IsUnit b
-- Mathlib/Data/ZMod/Basic.lean
theorem neg_val' {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = (n - a.val) % n :=
  calc
    (-a).val = val (-a) % n

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = (-a).val % n

Tactic:
rw [Nat.mod_eq_of_lt (-a).val_lt]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]

Tactic:
rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
  val_zero]

Result:
no goals
-- Mathlib/Data/Rat/Sqrt.lean
theorem sqrt_natCast (n : ℕ) : Rat.sqrt (n : ℚ) = Nat.sqrt n

Proof state:
n : ℕ
⊢ sqrt ↑n = ↑n.sqrt

Tactic:
rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp]
lemma rightHomologyMap'_op
    (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
let γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
simp only [γ.rightHomologyMap'_eq, γ.op.leftHomologyMap'_eq,
  RightHomologyMapData.op_φH]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_insert_eq_ite : #(insert a s) = if a ∈ s then #s else #s + 1

Proof state:
case neg
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
rw [card_insert_of_not_mem h, if_neg h]

Result:
no goals

Proof state:
case pos
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
rw [card_insert_of_mem h, if_pos h]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

case neg
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #(insert a s) = if a ∈ s then #s else #s + 1
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem valuation_p_pow_mul (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) :
    ((p : ℤ_[p]) ^ n * c).valuation = n + c.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ (↑p ^ n * c).valuation = n + c.valuation

Tactic:
rw [valuation_mul (NeZero.ne _) hc, valuation_pow, valuation_p, mul_one]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma formallyUnramified_algebraMap [Algebra R S] :
    (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S

Tactic:
delta FormallyUnramified

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S

Proof state:
case a.h.e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).toAlgebra = inst✝

Tactic:
exact Algebra.algebra_ext _ _ fun _ ↦ rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S

Tactic:
congr!

Result:
case a.h.e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).toAlgebra = inst✝
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem prod_eq_prod_mul_prod {α : Type*} [CommMonoid α] [NumberField K] (f : InfinitePlace K → α) :
    ∏ w, f w = (∏ w : {w // IsReal w}, f w.1) * (∏ w : {w // IsComplex w}, f w.1)

Proof state:
K : Type u_2
inst✝² : Field K
α : Type u_4
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w : InfinitePlace K, f w = (∏ w : { w // w.IsReal }, f ↑w) * ∏ w : { w // w.IsComplex }, f ↑w

Tactic:
rw [← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))]

Result:
K : Type u_2
inst✝² : Field K
α : Type u_4
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w : InfinitePlace K, f w =
    (∏ w : { w // w.IsReal }, f ↑w) * ∏ i : { x // ¬x.IsReal }, f ↑((Equiv.subtypeEquivRight ⋯) i)

Proof state:
K : Type u_2
inst✝² : Field K
α : Type u_4
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w : InfinitePlace K, f w =
    (∏ w : { w // w.IsReal }, f ↑w) * ∏ i : { x // ¬x.IsReal }, f ↑((Equiv.subtypeEquivRight ⋯) i)

Tactic:
simp [Fintype.prod_subtype_mul_prod_subtype]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_self : a ∆ a = ⊥

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ a = ⊥

Tactic:
rw [symmDiff, sup_idem, sdiff_self]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Multiset.trop_inf [LinearOrder R] [OrderTop R] (s : Multiset R) :
    trop s.inf = Multiset.sum (s.map trop)

Proof state:
case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = (map trop 0).sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : R
x : Multiset R
IH : trop x.inf = (map trop x).sum
⊢ trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum

Tactic:
simp [← IH]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset R
⊢ trop s.inf = (map trop s).sum

Tactic:
induction' s using Multiset.induction with s x IH

Result:
case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = (map trop 0).sum

case cons
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : R
x : Multiset R
IH : trop x.inf = (map trop x).sum
⊢ trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_of_getElem?_eq_some {xs : List α} (w : xs[xs.findIdx p]? = some y) : p y

Proof state:
case nil
α : Type u_1
p : α → Bool
y : α
w : [][findIdx p []]? = some y
⊢ p y = true

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
y x : α
xs : List α
ih : xs[findIdx p xs]? = some y → p y = true
w : (x :: xs)[findIdx p (x :: xs)]? = some y
⊢ p y = true

Tactic:
by_cases h : p x <;> simp_all [findIdx_cons]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
y : α
xs : List α
w : xs[findIdx p xs]? = some y
⊢ p y = true

Tactic:
induction xs with
| nil => simp_all
| cons x xs ih => by_cases h : p x <;> simp_all [findIdx_cons]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isCycle_copy {u u'} (p : G.Walk u u) (hu : u = u') :
    (p.copy hu hu).IsCycle ↔ p.IsCycle

Proof state:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
⊢ (p.copy hu hu).IsCycle ↔ p.IsCycle

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_max_zero (δ : ℝ) (E : Set α) : cthickening (max 0 δ) E = cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (0 ⊔ δ) E = cthickening δ E

Tactic:
cases le_total δ 0 <;> simp [cthickening_of_nonpos, *]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi : sin π = 0

Proof state:
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ sin π = 0

Tactic:
rw [← mul_div_cancel_left₀ π (two_ne_zero' ℝ), two_mul, add_div, sin_add, cos_pi_div_two]

Result:
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The gaussian pdf is nonnegative. -/
lemma gaussianPDFReal_nonneg (μ : ℝ) (v : ℝ≥0) (x : ℝ) : 0 ≤ gaussianPDFReal μ v x

Proof state:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ 0 ≤ gaussianPDFReal μ v x

Tactic:
rw [gaussianPDFReal]

Result:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ 0 ≤ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))

Proof state:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ 0 ≤ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))

Tactic:
positivity

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
theorem prod_fermatNumber (n : ℕ) : ∏ k ∈ range n, fermatNumber k = fermatNumber n - 2

Proof state:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2

Tactic:
ring_nf

Result:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ 2 ^ (2 ^ n * 2) - 1 = 1 + 2 ^ (2 ^ n * 2) - 2

Proof state:
case zero

⊢ ∏ k ∈ range 0, k.fermatNumber = fermatNumber 0 - 2

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2

Tactic:
induction n with | zero => rfl | succ n hn =>
rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
  (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by omega), ← sq_sub_sq]
ring_nf
omega

Result:
no goals

Proof state:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1

Tactic:
omega

Result:
no goals

Proof state:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ 2 ^ (2 ^ n * 2) - 1 = 1 + 2 ^ (2 ^ n * 2) - 2

Tactic:
omega

Result:
no goals

Proof state:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ ∏ k ∈ range (n + 1), k.fermatNumber = (n + 1).fermatNumber - 2

Tactic:
rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
  (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by omega), ← sq_sub_sq]

Result:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
    List.Pairwise R (l.flatMap f) ↔
      (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l

Proof state:
β : Type u_1
α : Type u_2
R : β → β → Prop
l : List α
f : α → List β
⊢ Pairwise R (flatMap f l) ↔
    (∀ (a : α), a ∈ l → Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ (x : β), x ∈ f a₁ → ∀ (y : β), y ∈ f a₂ → R x y) l

Tactic:
simp [List.flatMap, pairwise_flatten, pairwise_map]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem Spec_iff {R S : CommRingCat.{u}} {φ : R ⟶ S} :
    P (Spec.map φ) ↔ Q φ.hom

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
  ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
R S : CommRingCat
φ : R ⟶ S
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
have H := (isLocal_ringHomProperty P).respectsIso

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_addY (P Q : Fin 3 → A) : (W'.baseChange B).toJacobian.addY (f ∘ P) (f ∘ Q) =
    f ((W'.baseChange A).toJacobian.addY P Q)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toJacobian.addY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toJacobian.addY P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addY, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldl_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
g : γ → β → γ
x : γ
⊢ foldl g x (pmap f l H) = foldl (fun acc a => g acc (f a.val ⋯)) x l.attach

Tactic:
rw [pmap_eq_map_attach, foldl_map]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem isIso_π_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasLimit F] :
    IsIso (limit.π F j) :=
  ⟨⟨limit.lift _ (coneOfDiagramInitial I F), ⟨by ext; simp, by simp⟩⟩⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)

Tactic:
ext

Result:
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝

Proof state:
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.lift F (coneOfDiagramInitial I F) ≫ limit.π F j = 𝟙 (F.obj j)

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem induction_on_adjoin_fg (P : IntermediateField F E → Prop) (base : P ⊥)
    (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F))
    (K : IntermediateField F E) (hK : K.FG) : P K

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)
S : Finset E
⊢ P (adjoin F ↑S)

Tactic:
exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)
K : IntermediateField F E
hK : K.FG
⊢ P K

Tactic:
obtain ⟨S, rfl⟩ := hK

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)
S : Finset E
⊢ P (adjoin F ↑S)
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_isEmpty [IsEmpty n] {A : Matrix n n R} : permanent A = 1

Proof state:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty n
A : Matrix n n R
⊢ A.permanent = 1

Tactic:
simp [permanent]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_inter_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : 𝓝[s ∩ t] a = 𝓝[t] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a

Tactic:
exact nhdsWithin_le_of_mem h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s ∩ t] a = 𝓝[t] a

Tactic:
rw [nhdsWithin_inter, inf_eq_right]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem prod_X_sub_C_eq [CommRing S] {x y z : S} :
    (X - C x) * (X - C y) * (X - C z) =
      toPoly ⟨1, -(x + y + z), x * y + x * z + y * z, -(x * y * z)⟩

Proof state:
S : Type u_2
inst✝ : CommRing S
x y z : S
⊢ (X - C x) * (X - C y) * (X - C z) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly

Tactic:
rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
theorem induction_on {p : AdicCompletion I M → Prop} (x : AdicCompletion I M)
    (h : ∀ (f : AdicCauchySequence I M), p (mk I M f)) : p x

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : AdicCompletion I M → Prop
h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)
f : AdicCauchySequence I M
⊢ p ((mk I M) f)

Tactic:
exact h f

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : AdicCompletion I M → Prop
x : AdicCompletion I M
h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)
⊢ p x

Tactic:
obtain ⟨f, rfl⟩ := mk_surjective I M x

Result:
case intro
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : AdicCompletion I M → Prop
h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)
f : AdicCauchySequence I M
⊢ p ((mk I M) f)
-- Mathlib/RingTheory/Nilpotent/Basic.lean
protected lemma isNilpotent_mul_left_iff (h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsLeft R) :
    IsNilpotent (x * y) ↔ IsNilpotent x

Proof state:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent x

Tactic:
rw [mul_pow h_comm] at hk

Result:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent x

Proof state:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent x

Tactic:
exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hy k _ hk⟩

Result:
no goals

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) → IsNilpotent x

Tactic:
rintro ⟨k, hk⟩

Result:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent x

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) ↔ IsNilpotent x

Tactic:
refine ⟨?_, h_comm.isNilpotent_mul_left⟩

Result:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) → IsNilpotent x
-- Mathlib/NumberTheory/Ostrowski.lean
/-- Given two natural numbers `n, m` greater than 1 we have `f n ≤ f m ^ logb m n`. -/
lemma le_pow_log : f n ≤ f m ^ logb m n

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ Tendsto (fun k => (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n) atTop (𝓝 (1 * f ↑m ^ logb ↑m ↑n))

Tactic:
exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ↑n ≤ f ↑m ^ logb ↑m ↑n

Tactic:
have : Tendsto (fun k : ℕ ↦ (m * f m / (f m - 1)) ^ (k : ℝ)⁻¹ * f m ^ logb m n)
    atTop (𝓝 (f m ^ logb m n)) := by
  nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]
  exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _

Result:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
this : Tendsto (fun k => (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n) atTop (𝓝 (f ↑m ^ logb ↑m ↑n))
⊢ f ↑n ≤ f ↑m ^ logb ↑m ↑n

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ Tendsto (fun k => (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n) atTop (𝓝 (f ↑m ^ logb ↑m ↑n))

Tactic:
nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]

Result:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ Tendsto (fun k => (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n) atTop (𝓝 (1 * f ↑m ^ logb ↑m ↑n))

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
this : Tendsto (fun k => (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n) atTop (𝓝 (f ↑m ^ logb ↑m ↑n))
⊢ f ↑n ≤ f ↑m ^ logb ↑m ↑n

Tactic:
exact le_of_tendsto_of_tendsto (tendsto_const_nhds (x:= f ↑n)) this <|
  eventually_atTop.mpr ⟨2, fun b hb ↦ param_upperbound hm hn notbdd (not_eq_zero_of_lt hb)⟩

Result:
no goals