mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℤ
⊢ f ↑n ≤ 1

Tactic:
by
  obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n <;>
  simp [apply_natCast_le_one hna]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
h_lt : f y < f x
⊢ f (x + y) = max (f x) (f y)

Tactic:
add_eq_left_of_lt hna h_lt

Goal state after:
case inr
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
h_lt : f y < f x
⊢ f x = max (f x) (f y)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s : Finset β
hnonempty : s.Nonempty
l : β → α
⊢ f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun i ↦ f (l i)

Tactic:
induction hnonempty using Nonempty.cons_induction with
  | singleton i => simp
  | cons i s _ hs hind =>
    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
    rw [← le_sup'_iff hs]
    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
    · exact .inl h₁
    · exact .inr <| le_trans h₂ hind

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
⊢ ArchimedeanClass.mk ↑(f (f.support.min' hsupport)) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
seed.archimedeanClassMk_of_mem_stratum (f _).prop
    (by simpa using! f.support.min'_mem hsupport)

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x : R⟦Γ⟧
⊢ 1 * x = x

Tactic:
by
    ext
    exact coeff_single_zero_mul.trans (one_mul _)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
⊢ ∀ {a b : R⟦Γ⟧ˣ},
    a ∈ {x | 0 < (↑x - 1).orderTop} → b ∈ {x | 0 < (↑x - 1).orderTop} → a * b ∈ {x | 0 < (↑x - 1).orderTop}

Tactic:
by
    intro x y hx hy
    obtain (_ | _) := subsingleton_or_nontrivial R
    · simp
    · simp_all only [Set.mem_ofPred_eq, orderTop_self_sub_one_pos_iff]
      have h1 : x.val.leadingCoeff * y.val.leadingCoeff = 1 := by rw [hx.2, hy.2, mul_one]
      constructor
      · rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]
      · rw [Units.val_mul, leadingCoeff_mul_of_ne_zero (h1 ▸ one_ne_zero), h1]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁷ : AddCommMonoid Γ
inst✝⁶ : PartialOrder Γ
inst✝⁵ : IsOrderedCancelAddMonoid Γ
inst✝⁴ : CommSemiring R
A : Type u_6
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Nontrivial Γ
inst✝ : Nontrivial R
a : Γ
ha : a ≠ 0
x : R
⊢ ¬((single 0) ((algebraMap R R) x)).coeff a = 1

Tactic:
coeff_single_of_ne ha

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁷ : AddCommMonoid Γ
inst✝⁶ : PartialOrder Γ
inst✝⁵ : IsOrderedCancelAddMonoid Γ
inst✝⁴ : CommSemiring R
A : Type u_6
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Nontrivial Γ
inst✝ : Nontrivial R
a : Γ
ha : a ≠ 0
x : R
⊢ ¬0 = 1
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
⊢ (Function.support (f.evalCoeff x)).IsWF

Tactic:
Set.isWF_iff_no_descending_seq

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
⊢ ∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ Function.support (f.evalCoeff x)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
hmem' : ∀ (n : ℕ), seq n ∈ Function.support (ofLex (↑↑f y)).coeff
hwf : True
⊢ ¬(ofLex (↑↑f y)).support.IsWF

Tactic:
Set.isWF_iff_no_descending_seq

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
hmem' : ∀ (n : ℕ), seq n ∈ Function.support (ofLex (↑↑f y)).coeff
hwf : True
⊢ ¬∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ (ofLex (↑↑f y)).support
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| f a - f b = f (a - b)

Tactic:
lhs; rw [← tsub_add_cancel_of_le h]

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| f (a - b + b) - f b
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x⁻¹ + 1 = 0
⊢ x ∈ B

Tactic:
rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2

Goal state after:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x = -1
⊢ x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker
⊢ ↑(A.unitGroupMulEquiv.symm ↑x) ∈ A.principalUnitGroup

Tactic:
by
      rw [A.coe_mem_principalUnitGroup_iff]; simp

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K d
⊢ ↑(ball K d) ⊆ ↑(ball K c)

Tactic:
by simpa using (ball_strictAnti K).antitone hdc

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Subsingleton R
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
simp only [isMonicOfDegree_iff_of_subsingleton, mul_eq_zero] at hp ⊢

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hq : q.IsMonicOfDegree n
h : Subsingleton R
hp : m = 0
⊢ m = 0 ∨ n = 0
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p - q).IsMonicOfDegree n

Tactic:
rw [sub_eq_add_neg]
  exact hp.add_right <| (natDegree_neg q) ▸ hq

Goal state after:
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ (a • p).mirror = a • p.mirror

Tactic:
by
  rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]

Goal state after:
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ Irreducible p

Tactic:
Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three hdeg2 hdeg.2

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ p.roots = 0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
⊢ ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations

Tactic:
have h₂ : eraseLead ((X - C η) * monomial d c) ≠ 0 := by
    apply mt nextCoeff_eq_zero_of_eraseLead_eq_zero
    simp [h₁, hc, hη.ne']

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
h₂ : ((X - C η) * (monomial d) c).eraseLead ≠ 0
⊢ ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
p q : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
hkm' : k < m
hmn' : m < n
hq : q = trinomial k m n ↑u ↑v ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
exact Or.inl (hq.trans hp.symm)

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : x * (star x * (algebraMap R (QuadraticAlgebra R a b)) r) = 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
refine ⟨_, hr, ?_⟩

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : x * (star x * (algebraMap R (QuadraticAlgebra R a b)) r) = 1
hr' : r * norm x = 1
⊢ star x * (algebraMap R (QuadraticAlgebra R a b)) r * x = 1
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

Tactic:
rintro rfl; rfl

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
h : IsInvolutory R
x y : R
⊢ x ◃⁻¹ y = x ◃ y

Tactic:
rw [← left_cancel x, right_inv, h x]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ R[B.i, B.j, B.k] ≤ B.liftHom.range

Tactic:
· rw [Algebra.adjoin_le_iff]
    rintro x (rfl | rfl | rfl)
      <;> [use (Basis.self R).i; use (Basis.self R).j; use (Basis.self R).k]
    all_goals simp [lift]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.refl
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ : R
⊢ Relation.EqvGen (Rel r) x✝ x✝

Tactic:
exact (RingQuot.ringCon r).refl _

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ Function.Surjective ⇑(mkAlgHom S s)

Tactic:
suffices Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s) by
    simpa [mkAlgHom_def, mkRingHom_def]

Goal state after:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ Function.Surjective fun x ↦ { toQuot := Quot.mk (Rel s) x }
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : { f // ∀ ⦃x y : A⦄, s x y → f x = f y }
⊢ (fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) ((fun f' ↦ preLiftAlgHom S ⋯) f) = f

Tactic:
ext
      simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def,
        AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single.single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
h : SkewMonoidAlgebra k G
x : G
a : k
y : G
b : k
⊢ single x a * single y b * h = single x a * (single y b * h)

Tactic:
induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
⊢ ∀ x_1 ∈ x.coeff.support, (if x_1 * g = g' then x.coeff x_1 * x_1 • r else 0) = 0

Tactic:
ite_eq_right_iff

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
⊢ ∀ x_1 ∈ x.coeff.support, x_1 * g = g' → x.coeff x_1 * x_1 • r = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ ∀ x_1 ∈ x.coeff.support, (if g * x_1 = g' then r * g • x.coeff x_1 else 0) = 0

Tactic:
ite_eq_right_iff

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ ∀ x_1 ∈ x.coeff.support, g * x_1 = g' → r * g • x.coeff x_1 = 0
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ Hom.stalkMap (α ≫ β) x = Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x

Tactic:
dsimp [Hom.stalkMap, stalkFunctor, stalkPushforward]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ colimMap ((OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op.whiskerLeft (α ≫ β).c) ≫
      colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
        colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    (colimMap
          ((OpenNhds.inclusion ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op.whiskerLeft β.c) ≫
        colimMap
            (whiskerRight
              (𝟙
                (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x) ⋙
                    OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op)
              Y.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op ⋙ Y.presheaf)
            (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x)).op) ≫
      colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op.whiskerLeft α.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝¹ : Category.{v', u'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑↑(F.obj j₃))ᵒᵖ
⊢ (F.map (f ≫ g)).c.app U =
    (F.map g).c.app U ≫
      ((pushforward C (F.map g).base).map (F.map f).c).app U ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U

Tactic:
simp [PresheafedSpace.congr_app (F.map_comp f g)]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
rwa [this, types_comp, types_comp, Function.comp_assoc, Set.range_comp,
      Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _), Set.image_univ,
      Types.range_pullbackFst]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
have := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H
  have : IsIso (pullback.snd f g).base := by
    delta pullback.snd
    rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
    change IsIso (_ ≫ pullback.snd _ _)
    infer_instance
  apply to_iso

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (fst ≫ f) p = g (snd p)

Tactic:
h.w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (snd ≫ g) p = g (snd p)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ x ∈
    Set.range
      ⇑({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
          1)

Tactic:
Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp _)

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ x ∈ Set.univ

X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ Epi
    ({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
        1).base