harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Div.lean
theorem rootMultiplicity_eq_nat_find_of_nonzero [DecidableEq R] {p : R[X]} (p0 : p ≠ 0) {a : R} :
    letI : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
      have := decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1))
      inferInstanceAs (Decidable ¬_)
    rootMultiplicity a p = Nat.find (finiteMultiplicity_X_sub_C a p0)

Proof state:
case refl
R : Type u
inst✝ : Ring R
p : R[X]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯

Tactic:
rw [dif_neg p0]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯

Tactic:
cases Subsingleton.elim ‹DecidableEq R› (Classical.decEq R)

Result:
case refl
R : Type u
inst✝ : Ring R
p : R[X]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
p0 : p ≠ 0
a : R
⊢ rootMultiplicity a p = Nat.find ⋯

Tactic:
dsimp [rootMultiplicity]

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯
-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndep_iff (m' m₁ m₂ : MeasurableSpace Ω)
    {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω]
    (hm' : m' ≤ mΩ) (hm₁ : m₁ ≤ mΩ) (hm₂ : m₂ ≤ mΩ) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndep m' m₁ m₂ hm' μ
      ↔ ∀ t1 t2, MeasurableSet[m₁] t1 → MeasurableSet[m₂] t2
        → (μ⟦t1 ∩ t2 | m'⟧) =ᵐ[μ] (μ⟦t1 | m'⟧) * (μ⟦t2 | m'⟧)

Proof state:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']

Tactic:
rw [condIndep_iff_condIndepSets, condIndepSets_iff]

Result:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ {s | MeasurableSet s} →
        t2 ∈ {s | MeasurableSet s} →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']

case hs1
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Proof state:
case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
exact hm₂

Result:
no goals

Proof state:
case hs1
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
exact hm₁

Result:
no goals

Proof state:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ {s | MeasurableSet s} →
        t2 ∈ {s | MeasurableSet s} →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getCast_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {h} :
    l.getCast a h = getValueCast a l.toList (contains_eq.symm.trans h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k : α
v : β k
t : AssocList α β
ih : ∀ {h : contains a t = true}, getCast a t h = getValueCast a t.toList ⋯
h : contains a (cons k v t) = true
⊢ getCast a (cons k v t) h = getValueCast a (cons k v t).toList ⋯

Tactic:
simp only [getCast, toList_cons, List.getValueCast_cons, ih]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : ∀ {h : contains a tail✝ = true}, getCast a tail✝ h = getValueCast a tail✝.toList ⋯
h : contains a (cons key✝ value✝ tail✝) = true
⊢ getCast a (cons key✝ value✝ tail✝) h = getValueCast a (cons key✝ value✝ tail✝).toList ⋯

Tactic:
next k v t ih => simp only [getCast, toList_cons, List.getValueCast_cons, ih]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : AssocList α β
a : α
h : contains a l = true
⊢ getCast a l h = getValueCast a l.toList ⋯

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : contains a nil = true
⊢ getCast a nil h = getValueCast a nil.toList ⋯

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : ∀ {h : contains a tail✝ = true}, getCast a tail✝ h = getValueCast a tail✝.toList ⋯
h : contains a (cons key✝ value✝ tail✝) = true
⊢ getCast a (cons key✝ value✝ tail✝) h = getValueCast a (cons key✝ value✝ tail✝).toList ⋯

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : contains a nil = true
⊢ getCast a nil h = getValueCast a nil.toList ⋯

Tactic:
simp [contains] at h

Result:
no goals
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem tendsto_iff_tendstoUniformlyOn {ι : Type*} {p : Filter ι} [UniformSpace F]
    [UniformAddGroup F] (𝔖 : Set (Set E)) {a : ι → UniformConvergenceCLM σ F 𝔖}
    {a₀ : UniformConvergenceCLM σ F 𝔖} :
    Filter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (a · ·) a₀ p s

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
ι : Type u_5
p : Filter ι
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
a : ι → UniformConvergenceCLM σ F 𝔖
a₀ : UniformConvergenceCLM σ F 𝔖
⊢ (∀ s ∈ 𝔖,
      TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ a)
        ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) a₀)) p s) ↔
    ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 => (a x1) x2) (⇑a₀) p s

Tactic:
rfl

Result:
no goals

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
ι : Type u_5
p : Filter ι
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
a : ι → UniformConvergenceCLM σ F 𝔖
a₀ : UniformConvergenceCLM σ F 𝔖
⊢ Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 => (a x1) x2) (⇑a₀) p s

Tactic:
rw [(isEmbedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
ι : Type u_5
p : Filter ι
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
a : ι → UniformConvergenceCLM σ F 𝔖
a₀ : UniformConvergenceCLM σ F 𝔖
⊢ (∀ s ∈ 𝔖,
      TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ a)
        ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) a₀)) p s) ↔
    ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 => (a x1) x2) (⇑a₀) p s
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_eq_zero_iff_remainder {p r : ℕ} (i : ℕ) (pp : p.Prime) (hr0 : r ≠ 0) :
    ¬p ∣ r ↔ (p * i + r).factorization p = 0

Proof state:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0

Tactic:
refine ⟨pp, ?_, ?_⟩

Result:
case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Proof state:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r

Tactic:
contrapose! h

Result:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0

Proof state:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
⊢ ¬p ∣ r ↔ (p * i + r).factorization p = 0

Tactic:
refine ⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩

Result:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : (p * i + r).factorization p = 0
⊢ ¬p ∣ r

Proof state:
case refine_2
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0

Tactic:
exact (add_eq_zero.1 hr0).2

Result:
no goals

Proof state:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : (p * i + r).factorization p = 0
⊢ ¬p ∣ r

Tactic:
rw [factorization_eq_zero_iff] at h

Result:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r

Proof state:
case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

Tactic:
rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]

Result:
no goals

Proof state:
case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Tactic:
contrapose! hr0

Result:
case refine_2
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem contDiffOn_univBall_symm :
    ContDiffOn ℝ n (univBall c r).symm (ball c r)

Proof state:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ Set.MapsTo (↑(unitBallBall c r h).symm) (ball c r) (ball 0 1)

Tactic:
rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]

Result:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ Set.MapsTo (↑(unitBallBall c r h).symm) (unitBallBall c r h).target (unitBallBall c r h).source

Proof state:
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ (↑n) (↑(IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph.symm) (ball c r)

Tactic:
exact contDiffOn_id.sub contDiffOn_const

Result:
no goals

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ (↑n) (↑(univBall c r).symm) (ball c r)

Tactic:
unfold univBall

Result:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ (↑n)
    (↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph).symm)
    (ball c r)

Proof state:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ Set.MapsTo (↑(unitBallBall c r h).symm) (unitBallBall c r h).target (unitBallBall c r h).source

Tactic:
apply PartialHomeomorph.symm_mapsTo

Result:
no goals

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ (↑n)
    (↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph).symm)
    (ball c r)

Tactic:
split_ifs with h

Result:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ (↑n) (↑(univUnitBall.trans' (unitBallBall c r h) ⋯).symm) (ball c r)

case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ (↑n) (↑(IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph.symm) (ball c r)

Proof state:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ (↑n) (↑(univUnitBall.trans' (unitBallBall c r h) ⋯).symm) (ball c r)

Tactic:
refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_

Result:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ Set.MapsTo (↑(unitBallBall c r h).symm) (ball c r) (ball 0 1)
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto (hs : IsOpen s) :
    TendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) :=
  tendstoLocallyUniformlyOn_iff_forall_tendsto.trans <| forall₂_congr fun x hx => by
    rw [hs.nhdsWithin_eq hx]

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
hs : IsOpen s
x : α
hx : x ∈ s
⊢ Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) ↔ Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
rw [hs.nhdsWithin_eq hx]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_polynomial_iff_isJacobsonRing : IsJacobsonRing R[X] ↔ IsJacobsonRing R

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R[X] ↔ IsJacobsonRing R

Tactic:
refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩

Result:
R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R[X] → IsJacobsonRing R

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R[X] → IsJacobsonRing R

Tactic:
intro H

Result:
R : Type u_1
inst✝ : CommRing R
H : IsJacobsonRing R[X]
⊢ IsJacobsonRing R

Proof state:
R : Type u_1
inst✝ : CommRing R
H : IsJacobsonRing R[X]
⊢ IsJacobsonRing R

Tactic:
exact isJacobsonRing_of_surjective ⟨eval₂RingHom (RingHom.id _) 1, fun x =>
  ⟨C x, by simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]⟩⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
H : IsJacobsonRing R[X]
x : R
⊢ (eval₂RingHom (RingHom.id R) 1) (C x) = x

Tactic:
simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
lemma CompactIccSpace.mk'' [TopologicalSpace α] [PartialOrder α]
    (h : ∀ {a b : α}, a < b → IsCompact (Icc a b)) : CompactIccSpace α :=
  .mk' fun hab => hab.eq_or_lt.elim (by rintro rfl; simp) h

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ b✝ : α
hab : a✝ ≤ b✝
⊢ a✝ = b✝ → IsCompact (Icc a✝ b✝)

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
theorem to_product_injective_of_isLimit {D : Cone F} (hD : IsLimit D) :
    Function.Injective fun (x : ToType D.pt) (j : J) => D.π.app j x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Tactic:
change Function.Injective (T.hom ≫ fun x j => G.π.app j x)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
⊢ Function.Injective (T.hom ≫ fun x j => G.π.app j x)
-- Mathlib/Data/Nat/PartENat.lean
theorem add_lt_add_right {x y z : PartENat} (h : x < y) (hz : z ≠ ⊤) : x + z < y + z

Proof state:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ ↑m + ↑k < ↑n + ↑k

Tactic:
norm_cast

Result:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ m + k < n + k

Proof state:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : ↑m < ↑n
⊢ ↑m + ↑k < ↑n + ↑k

Tactic:
norm_cast at h

Result:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ ↑m + ↑k < ↑n + ↑k

Proof state:
x y z : PartENat
h : x < y
hz : z ≠ ⊤
⊢ x + z < y + z

Tactic:
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩

Result:
case intro
y z : PartENat
hz : z ≠ ⊤
m : ℕ
h : ↑m < y
⊢ ↑m + z < y + z

Proof state:
case intro
y z : PartENat
hz : z ≠ ⊤
m : ℕ
h : ↑m < y
⊢ ↑m + z < y + z

Tactic:
rcases ne_top_iff.mp hz with ⟨k, rfl⟩

Result:
case intro.intro
y : PartENat
m : ℕ
h : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
⊢ ↑m + ↑k < y + ↑k

Proof state:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑(m + k) < ⊤

Tactic:
apply natCast_lt_top

Result:
no goals

Proof state:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ m + k < n + k

Tactic:
apply add_lt_add_right h

Result:
no goals

Proof state:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤

Tactic:
norm_cast

Result:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑(m + k) < ⊤

Proof state:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤ + ↑k

Tactic:
rw [top_add]

Result:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤

Proof state:
case intro.intro
y : PartENat
m : ℕ
h : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
⊢ ↑m + ↑k < y + ↑k

Tactic:
induction' y using PartENat.casesOn with n

Result:
case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤ + ↑k

case intro.intro.a
m k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : ↑m < ↑n
⊢ ↑m + ↑k < ↑n + ↑k
-- Mathlib/NumberTheory/NumberField/Basic.lean
theorem isIntegral (x : 𝓞 K) : IsIntegral ℤ x

Proof state:
case intro.intro
K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0

Tactic:
rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0
⊢ IsIntegral ℤ x

Tactic:
refine ⟨P, hPm, ?_⟩

Result:
case intro.intro
K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0

Proof state:
K : Type u_1
inst✝ : Field K
x : 𝓞 K
⊢ IsIntegral ℤ x

Tactic:
obtain ⟨P, hPm, hP⟩ := x.isIntegral_coe

Result:
case intro.intro
K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0
⊢ IsIntegral ℤ x
-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem isSheaf_iff_isSheafUniqueGluing_types : F.IsSheaf ↔ F.IsSheafUniqueGluing

Proof state:
case refine_2
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
⊢ ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j

Tactic:
convert h

Result:
case h.e'_2.h.h.h.h.e'_3.h.e
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ s = objPairwiseOfFamily fun i => s (op (Pairwise.single i))

Proof state:
case h.e'_2.h.h.h.h.e'_3.h.e.h.op.pair
X : TopCat
F : Presheaf (Type u) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (Functor.mapCone F (Pairwise.cocone U).op).π.app i s_1 =
        objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) i
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i j : ι
⊢ s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun i => s (op (Pairwise.single i))) (op (Pairwise.pair i j))

Tactic:
exact (hs <| op <| Pairwise.Hom.left i j).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_assoc' (b : Int) {a c : Int}
    (h : c ∣ a) : (a * b) / c = a / c * b

Proof state:
b a c : Int
h : c ∣ a
⊢ a * b / c = a / c * b

Tactic:
rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
@[simp]
lemma rlp_pushouts : T.pushouts.rlp = T.rlp

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts.rlp ≤ T.rlp

Tactic:
exact antitone_rlp T.le_pushouts

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts ≤ T.rlp.llp

Tactic:
exact T.pushouts_le_llp_rlp

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.pushouts.rlp

Tactic:
rw [← le_llp_iff_le_rlp]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts ≤ T.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts.rlp = T.rlp

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts.rlp ≤ T.rlp

case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.pushouts.rlp