harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem prod_normalizedFactors {a : α} (ane0 : a ≠ 0) :
    Associated (normalizedFactors a).prod a

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod ~ᵤ a

Tactic:
rw [normalizedFactors, factors, dif_neg ane0]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (⇑normalize) (Classical.choose ⋯)).prod ~ᵤ a

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (⇑normalize) (Classical.choose ⋯)).prod ~ᵤ a

Tactic:
refine Associated.trans ?_ (Classical.choose_spec (exists_prime_factors a ane0)).2

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (⇑normalize) (Classical.choose ⋯)).prod ~ᵤ (Classical.choose ⋯).prod

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (⇑normalize) (Classical.choose ⋯)).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
rw [← Associates.mk_eq_mk_iff_associated, ← Associates.prod_mk, ← Associates.prod_mk,
  Multiset.map_map]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (Associates.mk ∘ ⇑normalize) (Classical.choose ⋯)).prod =
    (Multiset.map Associates.mk (Classical.choose ⋯)).prod

Proof state:
case e_a.e_f.h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ ⇑normalize) x✝ = Associates.mk x✝

Tactic:
rw [Function.comp_apply, Associates.mk_normalize]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (Associates.mk ∘ ⇑normalize) (Classical.choose ⋯)).prod =
    (Multiset.map Associates.mk (Classical.choose ⋯)).prod

Tactic:
congr 2

Result:
case e_a.e_f
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Associates.mk ∘ ⇑normalize = Associates.mk

Proof state:
case e_a.e_f
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Associates.mk ∘ ⇑normalize = Associates.mk

Tactic:
ext

Result:
case e_a.e_f.h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ ⇑normalize) x✝ = Associates.mk x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_ne_empty_iff [LawfulBEq α] {xs : Array α} {a : α} :
    xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : Array α
a : α
⊢ xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a]

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
xs : List α
⊢ { toList := xs }.erase a ≠ #[] ↔ { toList := xs } ≠ #[] ∧ { toList := xs } ≠ #[a]

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
xs : List α
⊢ { toList := xs }.erase a ≠ #[] ↔ { toList := xs } ≠ #[] ∧ { toList := xs } ≠ #[a]

Tactic:
simp [List.erase_ne_nil_iff]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem IsAntichain.minimal_mem_upperClosure_iff_mem (hs : IsAntichain (· ≤ ·) s) :
    Minimal (· ∈ upperClosure s) x ↔ x ∈ s

Proof state:
case refine_2
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x => ∃ a ∈ s, a ≤ x) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b

Tactic:
rwa [← hs.eq has h (hab.trans hbx)]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
h : Minimal (fun x => ∃ a ∈ s, a ≤ x) x
⊢ x ∈ s

Tactic:
obtain ⟨a, has, hax⟩ := h.prop

Result:
case refine_1.intro.intro
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
h : Minimal (fun x => ∃ a ∈ s, a ≤ x) x
a : α
has : a ∈ s
hax : a ≤ x
⊢ x ∈ s

Proof state:
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ Minimal (fun x => x ∈ upperClosure s) x ↔ x ∈ s

Tactic:
simp only [upperClosure, UpperSet.mem_mk, mem_setOf_eq]

Result:
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ Minimal (fun x => ∃ a ∈ s, a ≤ x) x ↔ x ∈ s

Proof state:
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ Minimal (fun x => ∃ a ∈ s, a ≤ x) x ↔ x ∈ s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩

Result:
case refine_1
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
h : Minimal (fun x => ∃ a ∈ s, a ≤ x) x
⊢ x ∈ s

case refine_2
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x => ∃ a ∈ s, a ≤ x) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b

Proof state:
case refine_1.intro.intro
α : Type u_1
x : α
s : Set α
inst✝ : PartialOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
h : Minimal (fun x => ∃ a ∈ s, a ≤ x) x
a : α
has : a ∈ s
hax : a ≤ x
⊢ x ∈ s

Tactic:
rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableOn.add_measure (hμ : IntegrableOn f s μ) (hν : IntegrableOn f s ν) :
    IntegrableOn f s (μ + ν)

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ ν : Measure α
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ Integrable f (μ.restrict s + ν.restrict s)

Tactic:
exact hμ.integrable.add_measure hν

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ ν : Measure α
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ IntegrableOn f s (μ + ν)

Tactic:
delta IntegrableOn

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ ν : Measure α
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ Integrable f ((μ + ν).restrict s)

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ ν : Measure α
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ Integrable f ((μ + ν).restrict s)

Tactic:
rw [Measure.restrict_add]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ ν : Measure α
hμ : IntegrableOn f s μ
hν : IntegrableOn f s ν
⊢ Integrable f (μ.restrict s + ν.restrict s)
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/--
The commutation isomorphisms of `Adjunction.LeftAdjointCommShift.iso` are compatible with
the unit of the adjunction.
-/
lemma compatibilityUnit_iso (a : A) :
    CommShift.CompatibilityUnit adj (iso adj a) (G.commShiftIso a)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctor C a).map ((shiftFunctorCompIsoId C a (-a) ⋯).inv.app (G.obj (F.obj X✝))) ≫
        (shiftFunctor C a).map ((shiftFunctor C (-a)).map ((G.commShiftIso a).inv.app (F.obj X✝))) ≫
          ((shiftFunctor C a).map (𝟙 ((G ⋙ shiftFunctor C (-a)).obj ((shiftFunctor D a).obj (F.obj X✝)))) ≫
              (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝)))) ≫
            (G.commShiftIso a).hom.app (F.obj X✝)

Tactic:
simp only [Functor.comp_obj, Functor.map_id, id_comp]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctor C a).map ((shiftFunctorCompIsoId C a (-a) ⋯).inv.app (G.obj (F.obj X✝))) ≫
        (shiftFunctor C a).map ((shiftFunctor C (-a)).map ((G.commShiftIso a).inv.app (F.obj X✝))) ≫
          (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝))) ≫
            (G.commShiftIso a).hom.app (F.obj X✝)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
⊢ CommShift.CompatibilityUnit adj (iso adj a) (G.commShiftIso a)

Tactic:
intro

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫ G.map ((iso adj a).hom.app X✝) ≫ (G.commShiftIso a).hom.app (F.obj X✝)
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_range_choose (n : ℕ) : (∑ m ∈ range (n + 1), n.choose m) = 2 ^ n

Proof state:
n : ℕ
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n

Tactic:
have := (add_pow 1 1 n).symm

Result:
n : ℕ
this : ∑ m ∈ range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(n.choose m) = (1 + 1) ^ n
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n

Proof state:
n : ℕ
this : ∑ m ∈ range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(n.choose m) = (1 + 1) ^ n
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n

Tactic:
simpa [one_add_one_eq_two] using this

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) :
    angle x (r • y) = angle x (-y)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ angle x (r • y) = angle x (-y)

Tactic:
rw [← neg_neg r, neg_smul, angle_neg_right, angle_smul_right_of_pos x y (neg_pos_of_neg hr),
  angle_neg_right]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.smul_const (hc : HasFDerivAt c c' x) (f : F) :
    HasFDerivAt (fun y => c y • f) (c'.smulRight f) x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : E
𝕜' : Type u_5
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
f : F
⊢ HasFDerivAt (fun y => c y • f) (c'.smulRight f) x

Tactic:
simpa only [smul_zero, zero_add] using hc.smul (hasFDerivAt_const f x)

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem of_injective_to_set {s : Set α} (hs : s ≠ Set.univ) {f : α → s} (hf : Injective f) :
    Infinite α :=
  of_not_fintype fun h => by
    classical
      refine lt_irrefl (Fintype.card α) ?_
      calc
        Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
        _ = #s.toFinset := s.toFinset_card.symm
        _ < Fintype.card α :=
          Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

Proof state:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α

Tactic:
calc
  Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
  _ = #s.toFinset := s.toFinset_card.symm
  _ < Fintype.card α :=
    Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False

Tactic:
classical
  refine lt_irrefl (Fintype.card α) ?_
  calc
    Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
    _ = #s.toFinset := s.toFinset_card.symm
    _ < Fintype.card α :=
      Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ s.toFinset ⊂ univ

Tactic:
rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False

Tactic:
refine lt_irrefl (Fintype.card α) ?_

Result:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.getThenInsertIfNew?_snd_val [BEq α] [Hashable α] {m : Raw₀ α (fun _ => β)} {a : α}
    {b : β} : (Raw.Const.getThenInsertIfNew? m.val a b).2 =
      (Raw₀.Const.getThenInsertIfNew? m a b).2.1

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
a : α
b : β
⊢ (Raw.Const.getThenInsertIfNew? m.val a b).snd = (Raw₀.Const.getThenInsertIfNew? m a b).snd.val

Tactic:
simp [Raw.Const.getThenInsertIfNew?, m.2]

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem AtPrime.Nontrivial [IsLocalization.AtPrime S P] : Nontrivial S :=
  nontrivial_of_ne (0 : S) 1 fun hze => by
    rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze
    obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze
    have htz : (t : R) = 0

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
htz : ↑t = 0
⊢ False

Tactic:
exact t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
⊢ False

Tactic:
have htz : (t : R) = 0 := by simpa using ht.symm

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
htz : ↑t = 0
⊢ False

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : 0 = 1
⊢ False

Tactic:
rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze

Result:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
⊢ False

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
⊢ ↑t = 0

Tactic:
simpa using ht.symm

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
⊢ False

Tactic:
obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
⊢ False
-- Mathlib/Data/Nat/PSub.lean
theorem psub'_eq_psub (m n) : psub' m n = psub m n

Proof state:
case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

Tactic:
exact (psub_eq_sub h).symm

Result:
no goals

Proof state:
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = m.psub n

Tactic:
split_ifs with h

Result:
case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Proof state:
m n : ℕ
⊢ m.psub' n = m.psub n

Tactic:
rw [psub']

Result:
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = m.psub n

Proof state:
case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
exact (psub_eq_none.2 (not_le.1 h)).symm

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_X_pow_add_C {n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n + C a) = n

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < (X ^ n).degree

Tactic:
rwa [degree_X_pow, Nat.cast_pos]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : (C a).degree < (X ^ n).degree
⊢ (X ^ n + C a).degree = ↑n

Tactic:
rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n + C a).degree = ↑n

Tactic:
have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by
  rwa [degree_X_pow, Nat.cast_pos]

Result:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : (C a).degree < (X ^ n).degree
⊢ (X ^ n + C a).degree = ↑n
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_functions_apply₁ {f : L.Functions 1} {t : L.Term α} {v : α → M} :
    (f.apply₁ t).realize v = funMap f ![t.realize v]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
i : Fin 1
⊢ realize v (![t] i) = ![realize v t] i

Tactic:
simp only [Matrix.cons_val_fin_one]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ (funMap f fun i => realize v (![t] i)) = funMap f ![realize v t]

Tactic:
refine congr rfl (funext fun i => ?_)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
i : Fin 1
⊢ realize v (![t] i) = ![realize v t] i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]

Tactic:
rw [Functions.apply₁, Term.realize]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ (funMap f fun i => realize v (![t] i)) = funMap f ![realize v t]
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_symm_X :
    matPolyEquiv.symm X = diagonal fun _ : n => (X : R[X])

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
this : (Matrix.map 1 fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X
⊢ matPolyEquiv.symm X = diagonal fun x => X

Tactic:
simpa [matPolyEquiv]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ((diagonal fun x => 1).map fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X

Tactic:
simp [-Matrix.diagonal_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ matPolyEquiv.symm X = diagonal fun x => X

Tactic:
suffices (Matrix.map 1 fun x ↦ X * algebraMap R R[X] x) = diagonal fun _ : n => (X : R[X]) by
  simpa [matPolyEquiv]

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ (Matrix.map 1 fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ (Matrix.map 1 fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X

Tactic:
rw [← Matrix.diagonal_one]

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ((diagonal fun x => 1).map fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_epi_imageToKernel : S.Exact ↔ Epi (imageToKernel S.f S.g S.zero)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ Epi (imageToKernel S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_imageToKernel']

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel' S.f S.g ⋯) ↔ Epi (imageToKernel S.f S.g ⋯)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel' S.f S.g ⋯) ↔ Epi (imageToKernel S.f S.g ⋯)

Tactic:
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Arrow.mk (imageToKernel' S.f S.g ⋯) ≅ Arrow.mk (imageToKernel S.f S.g ⋯)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Arrow.mk (imageToKernel' S.f S.g ⋯) ≅ Arrow.mk (imageToKernel S.f S.g ⋯)

Tactic:
exact Arrow.isoMk (imageSubobjectIso S.f).symm (kernelSubobjectIso S.g).symm

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_eq_sub (a b : α) : toIcoDiv hp a b = toIcoDiv hp 0 (b - a)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b = toIcoDiv hp 0 (b - a)

Tactic:
rw [toIcoDiv_sub_eq_toIcoDiv_add, zero_add]

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem trans_bot (f : α ≃. β) : f.trans (⊥ : β ≃. γ) = ⊥

Proof state:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
⊢ f.trans ⊥ = ⊥

Tactic:
ext

Result:
case h.a
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ a✝ ∈ (f.trans ⊥) x✝ ↔ a✝ ∈ ⊥ x✝

Proof state:
case h.a
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ a✝ ∈ (f.trans ⊥) x✝ ↔ a✝ ∈ ⊥ x✝

Tactic:
dsimp [PEquiv.trans]

Result:
case h.a
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ a✝ ∈ (f x✝).bind ⇑⊥ ↔ a✝ ∈ none

Proof state:
case h.a
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ a✝ ∈ (f x✝).bind ⇑⊥ ↔ a✝ ∈ none

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Pairwise.lean
theorem pairwise_iff_coe_toFinset_pairwise (hn : l.Nodup) (hs : Symmetric r) :
    (l.toFinset : Set α).Pairwise r ↔ l.Pairwise r

Proof state:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : l.Nodup
hs : Symmetric r
this : IsSymm α r := { symm := hs }
⊢ (↑l.toFinset).Pairwise r ↔ Pairwise r l

Tactic:
rw [coe_toFinset, hn.pairwise_coe]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : l.Nodup
hs : Symmetric r
⊢ (↑l.toFinset).Pairwise r ↔ Pairwise r l

Tactic:
letI : IsSymm α r := ⟨hs⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : l.Nodup
hs : Symmetric r
this : IsSymm α r := { symm := hs }
⊢ (↑l.toFinset).Pairwise r ↔ Pairwise r l
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_neg (s : SignedMeasure α) :
    (-s).toJordanDecomposition = -s.toJordanDecomposition

Proof state:
case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure

Tactic:
simp [toSignedMeasure_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition = -s.toJordanDecomposition

Tactic:
apply toSignedMeasure_injective

Result:
case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure