harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivWithinAt.mapsTo_tangent_cone {x : E} (h : HasFDerivWithinAt f f' s x) :
    MapsTo f' (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))

Proof state:
case intro.intro.intro.intro
𝕜 : 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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ f' v ∈ tangentConeAt 𝕜 (f '' s) (f x)

Tactic:
refine
  ⟨c, fun n => f (x + d n) - f x, mem_of_superset dtop ?_, clim, h.lim atTop dtop clim cdlim⟩

Result:
case intro.intro.intro.intro
𝕜 : 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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ {x_1 | (fun n => x + d n ∈ s) x_1} ⊆ {x_1 | (fun n => f x + (fun n => f (x + d n) - f x) n ∈ f '' s) x_1}

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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
⊢ MapsTo (⇑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))

Tactic:
rintro v ⟨c, d, dtop, clim, cdlim⟩

Result:
case intro.intro.intro.intro
𝕜 : 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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ f' v ∈ tangentConeAt 𝕜 (f '' s) (f x)

Proof state:
case intro.intro.intro.intro
𝕜 : 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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ {x_1 | (fun n => x + d n ∈ s) x_1} ⊆ {x_1 | (fun n => f x + (fun n => f (x + d n) - f x) n ∈ f '' s) x_1}

Tactic:
simp +contextual [-mem_image, mem_image_of_mem]

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem split_by_characteristic (h_pos : ∀ p : ℕ, p ≠ 0 → CharP R p → P) (h_equal : Algebra ℚ R → P)
    (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : p = 0
⊢ P

Tactic:
rw [h] at p_charP

Result:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
⊢ P

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
⊢ P

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : p = 0
⊢ P

case neg
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : ¬p = 0
⊢ P

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
⊢ P

Tactic:
haveI h0 : CharZero R := CharP.charP_to_charZero R

Result:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
h0 : CharZero R
⊢ P

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
h0 : CharZero R
⊢ P

Tactic:
exact split_equalCharZero_mixedCharZero R h_equal h_mixed

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : ¬p = 0
⊢ P

Tactic:
exact h_pos p h p_charP

Result:
no goals
-- Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
@[simp, reassoc, elementwise] lemma smoothSheafCommRing.ι_forgetStalk_inv (x : TopCat.of M) (U) :
    colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫
    (smoothSheafCommRing.forgetStalk IM I M R x).inv =
    ⇑(colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ (forgetStalk IM I M R x).inv =
    ⇑(ConcreteCategory.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U))

Tactic:
rw [Iso.comp_inv_eq, ← smoothSheafCommRing.ι_forgetStalk_hom]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ ⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      (forgetStalk IM I M R x).hom =
    ⇑(ConcreteCategory.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      (forgetStalk IM I M R x).hom

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ ⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      (forgetStalk IM I M R x).hom =
    ⇑(ConcreteCategory.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      (forgetStalk IM I M R x).hom

Tactic:
simp_rw [Functor.comp_obj, Functor.op_obj]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem of_right_adjoint {L : D ⥤ C} {R : C ⥤ D} (h : L ⊣ R) : IsFilteredOrEmpty D :=
  { cocone_objs := fun X Y =>
      ⟨R.obj (max (L.obj X) (L.obj Y)),
        h.homEquiv _ _ (leftToMax _ _), h.homEquiv _ _ (rightToMax _ _), ⟨⟩⟩
    cocone_maps := fun X Y f g =>
      ⟨R.obj (coeq (L.map f) (L.map g)), h.homEquiv _ _ (coeqHom _ _), by
        rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]⟩ }

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ f ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g)) =
    g ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g))

Tactic:
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
    (c : DefaultClause n) :
    c ∈ toList (insertRatUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
h :
  some c ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl : l ∈ (insertUnit acc unit).fst.toList
⊢ l ∈ f.ratUnits.toList ∨ l ∈ units

Tactic:
rw [insertUnit.eq_def] at hl

Result:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
h :
  some c ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl :
  l ∈
    (match acc with
        | (units, assignments, foundContradiction) =>
          match unit with
          | (l, b) =>
            let curAssignment := assignments[l.val]!;
            if hasAssignment b curAssignment = true then (units, assignments, foundContradiction)
            else
              (units.push (l, b), assignments.modify l.val (addAssignment b),
                foundContradiction || curAssignment != unassigned)).fst.toList
⊢ l ∈ f.ratUnits.toList ∨ l ∈ units
-- Mathlib/Topology/Basic.lean
theorem ContinuousAt.comp_of_eq {g : Y → Z} (hg : ContinuousAt g y)
    (hf : ContinuousAt f x) (hy : f x = y) : ContinuousAt (g ∘ f) x

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
x : X
y : Y
g : Y → Z
hg : ContinuousAt g y
hf : ContinuousAt f x
hy : f x = y
⊢ ContinuousAt (g ∘ f) x

Tactic:
subst hy

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x

Tactic:
exact hg.comp hf

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem lt_of_tsub_lt_tsub_right_of_le (h : c ≤ b) (h2 : a - c < b - c) : a < b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : c ≤ a
h2 : a - c < a - c
⊢ False

Tactic:
exact h2.false

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
h2 : a - c < b - c
⊢ a < b

Tactic:
refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
h2 : a - c < b - c
⊢ a ≠ b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
h2 : a - c < b - c
⊢ a ≠ b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : c ≤ a
h2 : a - c < a - c
⊢ False
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_lt_one_iff {x : R} : star x < 1 ↔ x < 1

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ star x < 1 ↔ x < 1

Tactic:
simpa using star_lt_star_iff (x := x) (y := 1)

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem isPathConnected_singleton (x : X) : IsPathConnected ({x} : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ ∀ {y : X}, y ∈ {x} → JoinedIn {x} x y

Tactic:
rintro y rfl

Result:
X : Type u_1
inst✝ : TopologicalSpace X
y : X
⊢ JoinedIn {y} y y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected {x}

Tactic:
refine ⟨x, rfl, ?_⟩

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ ∀ {y : X}, y ∈ {x} → JoinedIn {x} x y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
y : X
⊢ JoinedIn {y} y y

Tactic:
exact JoinedIn.refl rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_right_inj {x y : BitVec w} (z : BitVec w) : (z ^^^ x = z ^^^ y) ↔ x = y

Proof state:
w : Nat
x y z : BitVec w
⊢ x ^^^ z = y ^^^ z ↔ x = y

Tactic:
exact xor_left_inj _

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ z ^^^ x = z ^^^ y ↔ x = y

Tactic:
rw [xor_comm z x, xor_comm z y]

Result:
w : Nat
x y z : BitVec w
⊢ x ^^^ z = y ^^^ z ↔ x = y
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem factor_comp_mk (H : S ≤ T) : (factor H).comp (mk S) = mk T

Proof state:
case a
R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
x : R
⊢ ((factor H).comp (mk S)) x = (mk T) x

Tactic:
rw [RingHom.comp_apply, factor_mk]

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
⊢ (factor H).comp (mk S) = mk T

Tactic:
ext x

Result:
case a
R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
x : R
⊢ ((factor H).comp (mk S)) x = (mk T) x
-- Mathlib/Topology/Order.lean
theorem isClosed_sSup_iff {s : Set α} {T : Set (TopologicalSpace α)} :
    IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed[t] s

Proof state:
α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsClosed s ↔ ∀ t ∈ T, IsClosed s

Tactic:
simp only [sSup_eq_iSup, isClosed_iSup_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_negY (P : Fin 3 → A) :
    (W'.baseChange B).toJacobian.negY (f ∘ P) = f ((W'.baseChange A).toJacobian.negY P)

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 : Fin 3 → A
⊢ (baseChange W' B).toJacobian.negY (⇑f ∘ P) = f ((baseChange W' A).toJacobian.negY P)

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

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
lemma repr_eq_zero_of_nmem_range {i : ι} (hi : i ∉ Set.range snf.f) :
    snf.bM.repr m i = 0

Proof state:
case mk
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range ⇑snf.f
m : M
hm : m ∈ N
⊢ (snf.bM.repr ↑⟨m, hm⟩) i = 0

Tactic:
obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm

Result:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range ⇑snf.f
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) i = 0

Proof state:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hi : ∀ (j : Fin n), snf.f j ≠ i
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) i = 0

Tactic:
simp [Finsupp.single_apply, hi, snf.snf, map_finsupp_sum]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range ⇑snf.f
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ ∀ (j : Fin n), snf.f j ≠ i

Tactic:
simpa using hi

Result:
no goals

Proof state:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range ⇑snf.f
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) i = 0

Tactic:
replace hi : ∀ j, snf.f j ≠ i := by simpa using hi

Result:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hi : ∀ (j : Fin n), snf.f j ≠ i
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) i = 0

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : ι
hi : i ∉ range ⇑snf.f
⊢ (snf.bM.repr ↑m) i = 0

Tactic:
obtain ⟨m, hm⟩ := m

Result:
case mk
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range ⇑snf.f
m : M
hm : m ∈ N
⊢ (snf.bM.repr ↑⟨m, hm⟩) i = 0
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_pow' : ∀ {n : ℕ}, leadingCoeff p ^ n ≠ 0 → degree (p ^ n) = n • degree p
  | 0 => fun h => by rw [pow_zero, ← C_1] at *; rw [degree_C h, zero_nsmul]
  | n + 1 => fun h => by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Tactic:
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
rwa [pow_succ, ← leadingCoeff_pow' h₁] at h

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : 1 ≠ 0
⊢ (C 1).degree = 0 • p.degree

Tactic:
rw [degree_C h, zero_nsmul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Tactic:
rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff ^ 0 ≠ 0
⊢ (p ^ 0).degree = 0 • p.degree

Tactic:
rw [pow_zero, ← C_1] at *

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
h : 1 ≠ 0
⊢ (C 1).degree = 0 • p.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ (n + 1) = 0

Tactic:
rw [pow_succ, h₁, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Tactic:
have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by
  rwa [pow_succ, ← leadingCoeff_pow' h₁] at h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree