harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem fromSpec_preimage_self :
    hU.fromSpec ⁻¹ᵁ U = ⊤

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.fromSpec ⁻¹ᵁ U = ⊤

Tactic:
ext1

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ↑(hU.fromSpec ⁻¹ᵁ U) = ↑⊤

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ↑(hU.fromSpec ⁻¹ᵁ U) = ↑⊤

Tactic:
rw [Opens.map_coe, Opens.coe_top, ← hU.range_fromSpec, ← Set.image_univ]

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⇑(ConcreteCategory.hom hU.fromSpec.base) '' Set.univ) = Set.univ

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⇑(ConcreteCategory.hom hU.fromSpec.base) '' Set.univ) = Set.univ

Tactic:
exact Set.preimage_image_eq _ PresheafedSpace.IsOpenImmersion.base_open.injective

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
@[simp]
lemma add_eq_top : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : a + b = ⊤
nh : ¬(a = ⊤ ∨ b = ⊤)
⊢ False

Tactic:
rw [not_or] at nh

Result:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : a + b = ⊤
nh : ¬a = ⊤ ∧ ¬b = ⊤
⊢ False

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : b = ⊤
⊢ False

Tactic:
exact nh.2 h

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : (fun x => -a + x) (a + b) = (fun x => -a + x) ⊤
⊢ False

Tactic:
dsimp only at h

Result:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : -a + (a + b) = -a + ⊤
⊢ False

Proof state:
case mpr.inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
⊢ ⊤ + b = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case mpr.inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : -a + (a + b) = -a + ⊤
⊢ False

Tactic:
rw [add_top, ← add_assoc, add_comm (-a), add_neg_cancel_of_ne_top,
  zero_add] at h

Result:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : b = ⊤
⊢ False

case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : a + -a + b = ⊤
⊢ a ≠ ⊤

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ → a = ⊤ ∨ b = ⊤

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : a + b = ⊤
⊢ a = ⊤ ∨ b = ⊤

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : a + b = ⊤
⊢ a = ⊤ ∨ b = ⊤

Tactic:
by_contra nh

Result:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : a + b = ⊤
nh : ¬(a = ⊤ ∨ b = ⊤)
⊢ False

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
nh : ¬a = ⊤ ∧ ¬b = ⊤
h : a + -a + b = ⊤
⊢ a ≠ ⊤

Tactic:
exact nh.1

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a = ⊤ ∨ b = ⊤ → a + b = ⊤

Tactic:
rintro (rfl | rfl)

Result:
case mpr.inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
⊢ ⊤ + b = ⊤

case mpr.inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + ⊤ = ⊤

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ → a = ⊤ ∨ b = ⊤

case mpr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a = ⊤ ∨ b = ⊤ → a + b = ⊤
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow_of_exponent_nonpos {x y : ℝ} (hy : 0 < y) (hxy : y ≤ x) (hz : z ≤ 0) :
    x ^ z ≤ y ^ z

Proof state:
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ y ^ z

Tactic:
rcases ne_or_eq z 0 with hz_zero | rfl

Result:
case inl
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
⊢ x ^ z ≤ y ^ z

case inr
x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

Proof state:
case inr
x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

Tactic:
case inr => simp

Result:
no goals

Proof state:
z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z

Tactic:
simp

Result:
no goals

Proof state:
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
hxy' : x ≠ y
⊢ x ^ z ≤ y ^ z

Tactic:
exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy)
  (Ne.lt_of_le hz_zero hz)

Result:
no goals

Proof state:
x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case inl
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
hxy' : x ≠ y
⊢ x ^ z ≤ y ^ z

case inr
z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z

Tactic:
case inl =>
  exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy)
    (Ne.lt_of_le hz_zero hz)

Result:
case inr
z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z

Proof state:
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
⊢ x ^ z ≤ y ^ z

Tactic:
rcases ne_or_eq x y with hxy' | rfl

Result:
case inl
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
hxy' : x ≠ y
⊢ x ^ z ≤ y ^ z

case inr
z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z

Proof state:
case inr
z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z

Tactic:
case inr => simp

Result:
no goals

Proof state:
case inl
z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
⊢ x ^ z ≤ y ^ z

case inr
x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

Tactic:
case inl =>
  rcases ne_or_eq x y with hxy' | rfl
  case inl =>
    exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy)
      (Ne.lt_of_le hz_zero hz)
  case inr => simp

Result:
case inr
x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem mem_sSup_of_mem {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) :
    ∀ {x : M}, x ∈ s → x ∈ sSup S

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
have := le_sSup hs

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
rw [LE.le] at this

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : Preorder.toLE.1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : Preorder.toLE.1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
exact this

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- We have that `λ ^ (3*S.multiplicity-2)` divides `S.a + S.b`. -/
private lemma lambda_pow_dvd_a_add_b : λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h :
  λ ^ (3 * S.multiplicity - 2) * λ * λ ∣
    (S.a + S.b) * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S * λ * λ
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + S.b))

Tactic:
simp only [mul_dvd_mul_iff_right hζ.zeta_sub_one_prime'.ne_zero] at h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
h :
  λ ^ (3 * S.multiplicity - 2) ∣
    (S.a + S.b) * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + S.b))

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ S.multiplicity ∣ S.c
⊢ (λ ^ S.multiplicity) ^ 3 ∣ ↑S.u * S.c ^ 3

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem toPiLocalization_surjective_of_discreteTopology :
    Function.Surjective (toPiLocalization R) := fun x ↦ by
  have (p : PrimeSpectrum R) : ∃ f, (basicOpen f : Set _) = {p} :=
    have ⟨_, ⟨f, rfl⟩, hpf, hfp⟩ := isTopologicalBasis_basic_opens.isOpen_iff.mp
      (isOpen_discrete {p}) p rfl
    ⟨f, hfp.antisymm <| Set.singleton_subset_iff.mpr hpf⟩
  choose f hf using this
  let e := Equiv.ofInjective f fun p q eq ↦ Set.singleton_injective (hf p ▸ eq ▸ hf q)
  have loc a : IsLocalization.AtPrime (Localization.Away a.1) (e.symm a).1 :=
    (isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton <| hf _).mp <| by
      simp_rw [e, Equiv.apply_ofInjective_symm]; infer_instance
  let algE a := IsLocalization.algEquiv (e.symm a).1.primeCompl
    (Localization.AtPrime (e.symm a).1) (Localization.Away a.1)
  have span_eq : Ideal.span (Set.range f) = ⊤ := iSup_basicOpen_eq_top_iff.mp <| top_unique
    fun p _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨p, (hf p).ge rfl⟩
  replace hf a : (basicOpen a.1 : Set _) = {e.symm a}

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (f (e.symm a)) (Localization.Away ↑a)

Tactic:
simp_rw [e, Equiv.apply_ofInjective_symm]

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (↑a) (Localization.Away ↑a)
-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_coeff_one (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
    (v : Fin 1 → E) : (q.comp p) 1 v = q 1 fun _i => p 1 v

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : {Composition.ones 1} = Finset.univ
⊢ (q (Composition.ones 1).length) (p.applyComposition (Composition.ones 1) v) = (q 1) fun _i => (p 1) v

Tactic:
refine q.congr (by simp) fun i hi1 hi2 => ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : {Composition.ones 1} = Finset.univ
i : ℕ
hi1 : i < (Composition.ones 1).length
hi2 : i < 1
⊢ p.applyComposition (Composition.ones 1) v ⟨i, hi1⟩ = (p 1) v

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
⊢ {Composition.ones 1}.card = Fintype.card (Composition 1)

Tactic:
simp [composition_card]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
theorem leftOp {W : MorphismProperty C} {L : C ⥤ Dᵒᵖ} (h : W.IsInvertedBy L) :
    W.op.IsInvertedBy L.leftOp := fun X Y f hf => by
  haveI := h f.unop hf
  dsimp
  infer_instance

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).unop

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.leftOp.map f)

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).unop

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.leftOp.map f)

Tactic:
haveI := h f.unop hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.leftOp.map f)
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma coeff_preΨ'_ne_zero {n : ℕ} (h : (n : R) ≠ 0) :
    (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ ?m.92830 * ↑n ≠ 0

Tactic:
rwa [← Nat.cast_mul]

Result:
no goals

Proof state:
case intro.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n + 1) ≠ 0
⊢ (W.preΨ' (2 * n + 1)).coeff (((2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0

Tactic:
rwa [coeff_preΨ', if_neg n.not_even_two_mul_add_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑n ≠ 0
⊢ (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Result:
case intro.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ (W.preΨ' (2 * n)).coeff (((2 * n) ^ 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0

case intro.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n + 1) ≠ 0
⊢ (W.preΨ' (2 * n + 1)).coeff (((2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0

Proof state:
case intro.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ ↑n ≠ 0

Tactic:
exact right_ne_zero_of_mul <| by rwa [← Nat.cast_mul]

Result:
no goals

Proof state:
case intro.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ (W.preΨ' (2 * n)).coeff (((2 * n) ^ 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0

Tactic:
rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]

Result:
case intro.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ ↑n ≠ 0
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma coyoneda_exact₂ {X : C} (f : X ⟶ T.obj₂) (hf : f ≫ T.mor₂ = 0) :
    ∃ (g : X ⟶ T.obj₁), f = g ≫ T.mor₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ ∃ g, f = g ≫ T.mor₁

Tactic:
obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ T
  (contractible_distinguished X) hT f 0 (by aesop_cat)

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ ∃ g, f = g ≫ T.mor₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ (contractibleTriangle X).mor₂ ≫ 0 = f ≫ T.mor₂

Tactic:
aesop_cat

Result:
no goals

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ ∃ g, f = g ≫ T.mor₁

Tactic:
exact ⟨a, by simpa using ha₁⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ f = a ≫ T.mor₁

Tactic:
simpa using ha₁

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem IsOfFinOrder.of_mem_zpowers (h : IsOfFinOrder x) (h' : y ∈ Subgroup.zpowers x) :
    IsOfFinOrder y

Proof state:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
h' : y ∈ zpowers x
⊢ IsOfFinOrder y

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h'

Result:
case intro
G : Type u_1
inst✝ : Group G
x : G
h : IsOfFinOrder x
k : ℤ
h' : x ^ k ∈ zpowers x
⊢ IsOfFinOrder (x ^ k)

Proof state:
case intro
G : Type u_1
inst✝ : Group G
x : G
h : IsOfFinOrder x
k : ℤ
h' : x ^ k ∈ zpowers x
⊢ IsOfFinOrder (x ^ k)

Tactic:
exact h.zpow

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem toEven_ι (m : M) : (toEven Q (ι Q m) : CliffordAlgebra (Q' Q)) = e0 Q * v Q m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑((toEven Q) ((ι Q) m)) = e0 Q * (v Q) m

Tactic:
rw [toEven, CliffordAlgebra.lift_ι_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯) m) = e0 Q * (v Q) m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯) m) = e0 Q * (v Q) m

Tactic:
erw [LinearMap.codRestrict_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m = e0 Q * (v Q) m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m = e0 Q * (v Q) m

Tactic:
rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
lemma f_eq {i : ι} {i' : ι'} (h : e.f i = i') :
    f ψ i = (K.restrictionXIso e h).hom ≫ ψ.f i' ≫ (L.extendXIso e h).hom

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i : ι
i' : ι'
h : e.f i = i'
⊢ f ψ i = (K.restrictionXIso e h).hom ≫ ψ.f i' ≫ (L.extendXIso e h).hom

Tactic:
subst h

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i : ι
⊢ f ψ i = (K.restrictionXIso e ⋯).hom ≫ ψ.f (e.f i) ≫ (L.extendXIso e ⋯).hom

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i : ι
⊢ f ψ i = (K.restrictionXIso e ⋯).hom ≫ ψ.f (e.f i) ≫ (L.extendXIso e ⋯).hom

Tactic:
simp [f, restrictionXIso]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem differentiableAt_Gamma {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : DifferentiableAt ℝ Gamma s

Proof state:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ↑s ≠ -↑m

Tactic:
simp_rw [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]

Result:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ¬s = -↑m

Proof state:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℝ Gamma s

Tactic:
refine (Complex.differentiableAt_Gamma _ ?_).hasDerivAt.real_of_complex.differentiableAt

Result:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ↑s ≠ -↑m

Proof state:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ¬s = -↑m

Tactic:
exact hs

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Iic : (Iic b).map Fin.valEmbedding = Iic ↑b

Proof state:
n : ℕ
b : Fin n
⊢ map valEmbedding (Iic b) = Iic ↑b

Tactic:
simp [Iic_eq_finset_subtype, Finset.fin, Finset.map_map, Iic_filter_lt_of_lt_right]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation_self_right {x : V} (hx : x ≠ 0) (θ : Real.Angle) :
    o.oangle x (o.rotation θ x) = θ

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ o.oangle x ((o.rotation θ) x) = θ

Tactic:
simp [hx]

Result:
no goals