harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem lt_numLiterals {f : CNF Nat} (h : Mem v f) : v < numLiterals f

Proof state:
case h_1
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
h2 : f.maxLiteral = none
⊢ v < 0

Tactic:
exfalso

Result:
case h_1
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
h2 : f.maxLiteral = none
⊢ False

Proof state:
case h_2
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
n✝ : Nat
h2 : f.maxLiteral = some n✝
this : v ≤ n✝
⊢ v < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
case h_1
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
h2 : f.maxLiteral = none
⊢ False

Tactic:
apply of_maxLiteral_eq_none f h2 v h

Result:
no goals

Proof state:
v : Nat
f : CNF Nat
h : Mem v f
⊢ v < f.numLiterals

Tactic:
dsimp [numLiterals]

Result:
v : Nat
f : CNF Nat
h : Mem v f
⊢ v <
    match f.maxLiteral with
    | none => 0
    | some n => n + 1

Proof state:
case h_2
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
n✝ : Nat
h2 : f.maxLiteral = some n✝
⊢ v < n✝ + 1

Tactic:
have := of_maxLiteral_eq_some f h2 v h

Result:
case h_2
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
n✝ : Nat
h2 : f.maxLiteral = some n✝
this : v ≤ n✝
⊢ v < n✝ + 1

Proof state:
v : Nat
f : CNF Nat
h : Mem v f
⊢ v <
    match f.maxLiteral with
    | none => 0
    | some n => n + 1

Tactic:
split <;> rename_i h2

Result:
case h_1
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
h2 : f.maxLiteral = none
⊢ v < 0

case h_2
v : Nat
f : CNF Nat
h : Mem v f
x✝ : Option Nat
n✝ : Nat
h2 : f.maxLiteral = some n✝
⊢ v < n✝ + 1
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_C_ite [DecidableEq R] (a : R) : (C a).degree = if a = 0 then ⊥ else 0

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
a : R
⊢ (C a).degree = if a = 0 then ⊥ else 0

Tactic:
split_ifs with h <;> simp only [h, map_zero, degree_zero, degree_C, Ne, not_false_iff]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d

Proof state:
case intro.intro.top
d : ℝ≥0∞
a b : ℝ≥0
bd : ↑b < d
ac : ↑a < ⊤
⊢ ↑a + ↑b < ⊤ + d

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.coe.coe
a b x✝¹ : ℝ≥0
ac : ↑a < ↑x✝¹
x✝ : ℝ≥0
bd : ↑b < ↑x✝
⊢ ↑a + ↑b < ↑x✝¹ + ↑x✝

Tactic:
simp only [← coe_add, some_eq_coe, coe_lt_coe] at *

Result:
case intro.intro.coe.coe
a b x✝¹ x✝ : ℝ≥0
ac : a < x✝¹
bd : b < x✝
⊢ a + b < x✝¹ + x✝

Proof state:
case intro.intro.coe.coe
a b x✝¹ x✝ : ℝ≥0
ac : a < x✝¹
bd : b < x✝
⊢ a + b < x✝¹ + x✝

Tactic:
exact add_lt_add ac bd

Result:
no goals

Proof state:
case intro.intro.coe
d : ℝ≥0∞
a b : ℝ≥0
bd : ↑b < d
x✝ : ℝ≥0
ac : ↑a < ↑x✝
⊢ ↑a + ↑b < ↑x✝ + d

Tactic:
cases d

Result:
case intro.intro.coe.top
a b x✝ : ℝ≥0
ac : ↑a < ↑x✝
bd : ↑b < ⊤
⊢ ↑a + ↑b < ↑x✝ + ⊤

case intro.intro.coe.coe
a b x✝¹ : ℝ≥0
ac : ↑a < ↑x✝¹
x✝ : ℝ≥0
bd : ↑b < ↑x✝
⊢ ↑a + ↑b < ↑x✝¹ + ↑x✝

Proof state:
a b c d : ℝ≥0∞
ac : a < c
bd : b < d
⊢ a + b < c + d

Tactic:
lift a to ℝ≥0 using ac.ne_top

Result:
case intro
b c d : ℝ≥0∞
bd : b < d
a : ℝ≥0
ac : ↑a < c
⊢ ↑a + b < c + d

Proof state:
case intro.intro.coe.top
a b x✝ : ℝ≥0
ac : ↑a < ↑x✝
bd : ↑b < ⊤
⊢ ↑a + ↑b < ↑x✝ + ⊤

Tactic:
simp

Result:
no goals

Proof state:
case intro
b c d : ℝ≥0∞
bd : b < d
a : ℝ≥0
ac : ↑a < c
⊢ ↑a + b < c + d

Tactic:
lift b to ℝ≥0 using bd.ne_top

Result:
case intro.intro
c d : ℝ≥0∞
a : ℝ≥0
ac : ↑a < c
b : ℝ≥0
bd : ↑b < d
⊢ ↑a + ↑b < c + d

Proof state:
case intro.intro
c d : ℝ≥0∞
a : ℝ≥0
ac : ↑a < c
b : ℝ≥0
bd : ↑b < d
⊢ ↑a + ↑b < c + d

Tactic:
cases c

Result:
case intro.intro.top
d : ℝ≥0∞
a b : ℝ≥0
bd : ↑b < d
ac : ↑a < ⊤
⊢ ↑a + ↑b < ⊤ + d

case intro.intro.coe
d : ℝ≥0∞
a b : ℝ≥0
bd : ↑b < d
x✝ : ℝ≥0
ac : ↑a < ↑x✝
⊢ ↑a + ↑b < ↑x✝ + d
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometricSeries_apply_eq' (x : 𝔸) :
    (fun n => ordinaryHypergeometricSeries 𝔸 a b c n fun _ => x) =
      fun n => ((n !⁻¹ : 𝕂) * (ascPochhammer 𝕂 n).eval a * (ascPochhammer 𝕂 n).eval b *
        ((ascPochhammer 𝕂 n).eval c)⁻¹ ) • x ^ n

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
⊢ (fun n => (ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 => x) = fun n =>
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq']

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanIso.prod (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) :
    IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where
  bijOn := h₁.bijOn.prodMap h₂.bijOn
  map_prod_eq_map_prod s t hsA htA hs ht

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
⊢ ∀ ⦃x : α₂⦄, x ∈ map Prod.snd s → x ∈ A₂

Tactic:
simpa [@forall_swap α₁] using hsA.2

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
⊢ ∀ ⦃x : α₁⦄, x ∈ map Prod.fst t → x ∈ A₁

Tactic:
simpa using htA.1

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- Variant of `targetAffineLocally_affineAnd_iff` where `IsAffineHom` is bundled. -/
lemma targetAffineLocally_affineAnd_iff' (hQi : RingHom.RespectsIso Q)
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    targetAffineLocally (affineAnd Q) f ↔
      IsAffineHom f ∧ ∀ U : Y.Opens, IsAffineOpen U → Q (f.app U).hom

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
aesop

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [targetAffineLocally_affineAnd_iff hQi, isAffineHom_iff]

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem isSeparator_iff_faithful_preadditiveCoyoneda (G : C) :
    IsSeparator G ↔ (preadditiveCoyoneda.obj (op G)).Faithful

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveCoyoneda.obj (op G) ⋙ forget AddCommGrp).Faithful ↔ (preadditiveCoyoneda.obj (op G)).Faithful

Tactic:
exact ⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrp),
  fun h => Functor.Faithful.comp _ _⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ (preadditiveCoyoneda.obj (op G)).Faithful

Tactic:
rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj,
  whiskeringRight_obj_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveCoyoneda.obj (op G) ⋙ forget AddCommGrp).Faithful ↔ (preadditiveCoyoneda.obj (op G)).Faithful
-- Mathlib/Topology/StoneCech.lean
theorem ultrafilter_comap_pure_nhds (b : Ultrafilter α) : comap pure (𝓝 b) ≤ b

Proof state:
α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ ↑b

Tactic:
rw [TopologicalSpace.nhds_generateFrom]

Result:
α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 s) ≤ ↑b

Proof state:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s

Tactic:
refine iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_

Result:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s

Proof state:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ 𝓟 s

Tactic:
refine iInf_le_of_le { u | s ∈ u } ?_

Result:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s

Proof state:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i)

Tactic:
rw [← le_principal_iff]

Result:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ 𝓟 s

Proof state:
α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 s) ≤ ↑b

Tactic:
simp only [comap_iInf, comap_principal]

Result:
α : Type u
b : Ultrafilter α
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ ↑b

Proof state:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s

Tactic:
exact principal_mono.2 fun _ ↦ id

Result:
no goals

Proof state:
α : Type u
b : Ultrafilter α
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ ↑b

Tactic:
intro s hs

Result:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i)
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) enorm_zero] lemma enorm_one' : ‖(1 : E)‖ₑ = 0

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖ₑ = 0

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem exists_normalWord_prod_eq
    (d : TransversalPair G A B) (w : ReducedWord G A B) :
    ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧
      w'.toList.map Prod.fst = w.toList.map Prod.fst ∧
      ∀ u ∈ w.toList.head?.map Prod.fst,
      w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)

Proof state:
case mk.cons.intro.intro.intro.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ List.map Prod.fst ((t ^ ↑a.1 * of a.2) • w').toList =
      List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      ((t ^ ↑a.1 * of a.2) • w').head ∈ toSubgroup A B (-u)

Tactic:
have : ¬ Cancels a.1 (a.2 • w') := by
  simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some',
    Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
  intro hS x hx
  have hx' := congr_arg (Option.map Prod.fst) hx
  rw [← List.head?_map, hw'2, List.head?_map, Option.map_some'] at hx'
  have : w'.head ∈ toSubgroup A B a.fst := by
    simpa using hw'3 _ hx'
  rw [mul_mem_cancel_right this] at hS
  have : a.fst = -a.fst := by
    have hl : l ≠ [] := by rintro rfl; simp_all
    have : a.fst = (l.head hl).fst := (List.chain'_cons'.1 chain).1 (l.head hl)
      (List.head?_eq_head _) hS
    rwa [List.head?_eq_head hl, Option.map_some', ← this, Option.some_inj] at hx'
  simp at this

Result:
case mk.cons.intro.intro.intro.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
this : ¬Cancels a.1 (a.2 • w')
⊢ List.map Prod.fst ((t ^ ↑a.1 * of a.2) • w').toList =
      List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      ((t ^ ↑a.1 * of a.2) • w').head ∈ toSubgroup A B (-u)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
    a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

Tactic:
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem mul_inv_cancel : ∀ {p : RatFunc K}, p ≠ 0 → p * p⁻¹ = 1
  | ⟨p⟩, h => by
    have : p ≠ 0 := fun hp => h <| by rw [hp, ofFractionRing_zero]
    simpa only [← ofFractionRing_inv, ← ofFractionRing_mul, ← ofFractionRing_one,
        ofFractionRing.injEq] using
      mul_inv_cancel₀ this

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p } ≠ 0
hp : p = 0
⊢ { toFractionRing := p } = 0

Tactic:
rw [hp, ofFractionRing_zero]

Result:
no goals

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p } ≠ 0
⊢ { toFractionRing := p } * { toFractionRing := p }⁻¹ = 1

Tactic:
have : p ≠ 0 := fun hp => h <| by rw [hp, ofFractionRing_zero]

Result:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p } ≠ 0
this : p ≠ 0
⊢ { toFractionRing := p } * { toFractionRing := p }⁻¹ = 1

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p } ≠ 0
this : p ≠ 0
⊢ { toFractionRing := p } * { toFractionRing := p }⁻¹ = 1

Tactic:
simpa only [← ofFractionRing_inv, ← ofFractionRing_mul, ← ofFractionRing_one,
    ofFractionRing.injEq] using
  mul_inv_cancel₀ this

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_0_of_two_eq_zero (h2 : (2 : F) = 0) : ofJ 0 = ofJ0 F

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ ofJ 0 = ofJ0 F

Tactic:
rw [ofJ, if_pos rfl, if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ 3 = 1

Tactic:
linear_combination h2

Result:
no goals
-- Mathlib/Data/Prod/Lex.lean
theorem toLex_strictMono : StrictMono (toLex : α × β → α ×ₗ β)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Tactic:
obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt

Result:
case mk.mk.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ toLex (a₁, b₁) < toLex (a₁, b₂)

case mk.mk.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ StrictMono ⇑toLex

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h

Result:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Proof state:
case mk.mk.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ toLex (a₁, b₁) < toLex (a₁, b₂)

Tactic:
exact right _ (Prod.mk_lt_mk_iff_right.1 h)

Result:
no goals

Proof state:
case mk.mk.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Tactic:
exact left _ _ ha

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/BigOperators.lean
lemma series_ratio_test {f : ℕ → β} (n : ℕ) (r : α) (hr0 : 0 ≤ r) (hr1 : r < 1)
    (h : ∀ m, n ≤ m → abv (f m.succ) ≤ r * abv (f m)) :
    IsCauSeq abv fun m ↦ ∑ n ∈ range m, f n

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
generalize hk : m - n.succ = k

Result:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m - n.succ = k
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m - n.succ = k
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk

Result:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m = k + n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ ?m.150175 * r

Tactic:
rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn)

Result:
no goals
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem MemLp.exists_boundedContinuous_integral_rpow_sub_le [μ.WeaklyRegular] {p : ℝ} (hp : 0 < p)
    {f : α → E} (hf : MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) :
    ∃ g : α →ᵇ E, (∫ x, ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ MemLp g (ENNReal.ofReal p) μ

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal p) μ

Tactic:
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _

Result:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal p) μ

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal p) μ

Tactic:
have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp

Result:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal p) μ
-- Mathlib/Data/Rel.lean
theorem comp_right_top (r : Rel α β) : r • (⊤ : Rel β γ) = fun x _ ↦ x ∈ r.dom

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
z : γ
⊢ (r • ⊤) x z ↔ x ∈ r.dom

Tactic:
simp [comp, Top.top, dom]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ r • ⊤ = fun x x_1 => x ∈ r.dom

Tactic:
ext x z

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
z : γ
⊢ (r • ⊤) x z ↔ x ∈ r.dom
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_toList (s : Multiset α) : s.toList.prod = s.prod

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ s.toList.prod = (↑s.toList).prod

Tactic:
rw [prod_coe]

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ s.toList.prod = s.prod

Tactic:
conv_rhs => rw [← coe_toList s]

Result:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ s.toList.prod = (↑s.toList).prod
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
protected lemma isNilpotent_iff :
    IsNilpotent P ↔ ∀ i, IsNilpotent (coeff P i)

Proof state:
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
i : ℕ
⊢ IsNilpotent (C r)

Tactic:
obtain ⟨k, hk⟩ := hpr

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ IsNilpotent (C r)
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma isProbabilityMeasure (hf_bot : Tendsto f atBot (𝓝 0)) (hf_top : Tendsto f atTop (𝓝 1)) :
    IsProbabilityMeasure f.measure := ⟨by simp [f.measure_univ hf_bot hf_top]⟩

Proof state:
f : StieltjesFunction
hf_bot : Tendsto (↑f) atBot (𝓝 0)
hf_top : Tendsto (↑f) atTop (𝓝 1)
⊢ f.measure univ = 1

Tactic:
simp [f.measure_univ hf_bot hf_top]

Result:
no goals