mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
by
  obtain ⟨q, r, -, hf⟩ := eq_quo_mul_prod_add_sum_rem_mul_prod f
    (fun i hi => (hg i hi).pow (n i))
    (hgg.mono' fun i j hij => hij.pow)
  have hc (i : ι) : ∃ (q' : R[X]) (r' : Fin (n i) → R[X]), i ∈ s →
      (∀ j, (r' j).degree < (g i).degree) ∧
      r i = q' * g i ^ (n i) + ∑ j, r' j * g i ^ j.1 :=
    if hi : i ∈ s then
      (eq_quo_mul_pow_add_sum_rem_mul_pow (r i) (hg i hi) (n i)).elim
        fun q' h => h.elim fun r' h => ⟨q', r', fun _ => h⟩
    else
      ⟨0, fun _ => 0, hi.elim⟩
  choose q' r' hr' hr using hc
  refine ⟨q + ∑ i ∈ s, q' i, r', hr', hf.trans ?_⟩
  rw [add_mul, add_assoc, add_right_inj, Finset.sum_mul, ← Finset.sum_add_distrib]
  refine Finset.sum_congr rfl fun i hi => ?_
  rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ ⊥ < (g i ^ n i).degree

pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j * g i ^ ↑j).degree < (g i ^ n i).degree

Tactic:
· rw [bot_lt_iff_ne_bot, degree_ne_bot]
      exact ((hg i hi).pow (n i)).ne_zero

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j * g i ^ ↑j).degree < (g i ^ n i).degree
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x ◃ y = y ↔ y ◃ x = x

Tactic:
by
  grind [eq_mul_inv_iff_mul_eq]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹ ^ (0 + 1)
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)

Tactic:
zero_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹ ^ 1
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ x ∈ s, (algebraMap R[X] K) (r₁ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ (0 + 1) =
    (algebraMap R[X] K) q₂ + ∑ x ∈ s, (algebraMap R[X] K) (r₂ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ (0 + 1)

Tactic:
zero_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ x ∈ s, (algebraMap R[X] K) (r₁ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ 1 =
    (algebraMap R[X] K) q₂ + ∑ x ∈ s, (algebraMap R[X] K) (r₂ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ 1
Module: Mathlib.Algebra.Ring.Pointwise.Set

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ -x✝¹ * x✝ = -(x✝¹ * x✝)

Tactic:
by simp_rw [← image_neg_eq_neg]; exact image2_image_left_comm neg_mul

Goal state after:
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_1.inr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b

Tactic:
exact AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a + b) (a + c)

Tactic:
by
  rw [add_comm a b, add_comm a c]
  exact Rel.add_left h

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r a b
⊢ Rel r (a - c) (b - c)

Tactic:
by simp only [sub_eq_add_neg, h.add_left]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_4
inst✝⁵ : Monoid G
inst✝⁴ : Semiring A
inst✝³ : CommSemiring k
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
⊢ domCongrAlg k A ⋯ = AlgEquiv.refl

Tactic:
by
  apply AlgEquiv.ext
  aesop

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Monoid G
inst✝¹ : Semiring k
inst✝ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
⊢ f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

Tactic:
by
  rw [Fintype.mem_span_image_iff_exists_fun k]
  use Finset.restrict f.support f.coeff
  simp [smul_single, ← sum_def', sum_single]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial n) 1 = X ^ n

Tactic:
by
  induction n with
  | zero      => simp only [monomial_zero_left, ← CRingHom_eq_C, map_one, pow_zero]
  | succ n ih =>
    rw [pow_succ', ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial]
    simp [add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
a✝ : x✝ ∈ s
hx : x✝ ∉ p.support
⊢ f x✝ (p.coeff x✝) = 0

Tactic:
simp only [mem_support_iff, ne_eq, not_not] at hx

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
a✝ : x✝ ∈ s
hx : p.coeff x✝ = 0
⊢ f x✝ (p.coeff x✝) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) a + (monomial n) (-b) = (monomial n) a - (monomial n) b

Tactic:
monomial_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) a + -(monomial n) b = (monomial n) a - (monomial n) b
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: case add_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star (a✝¹ + c✝)) (Star.star (b✝ + c✝))

Tactic:
rw [star_add, star_add]

Goal state after:
case add_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star a✝¹ + Star.star c✝) (Star.star b✝ + Star.star c✝)
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: case mul_right
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star (a✝¹ * b✝)) (Star.star (a✝¹ * c✝))

Tactic:
rw [star_mul, star_mul]
                     exact Rel.mul_left h

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p : SkewMonoidAlgebra k G
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
coeff✝ : G →₀ k
⊢ { coeff := coeff✝ }.support = ∅ ↔ { coeff := coeff✝ } = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
inst✝ : DecidableEq G
p q : SkewMonoidAlgebra k G
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
simpa [support] using Finsupp.support_add

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddGroup k
a : SkewMonoidAlgebra k G
⊢ -a + a = 0

Tactic:
cases a; simp [← ofCoeff_neg, ← ofCoeff_add]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S₁ k
inst✝¹ : SMulZeroClass S₂ k
inst✝ : SMulCommClass S₁ S₂ k
x✝² : S₁
x✝¹ : S₂
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ x✝² • x✝¹ • { coeff := coeff✝ } = x✝¹ • x✝² • { coeff := coeff✝ }

Tactic:
by simp_rw [← ofCoeff_smul, smul_comm]

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
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2

Tactic:
let s := Set.Finite.toFinset (s := ({p : G × G | p.1 * p.2 = x}
    ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2)) this
  let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
  calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
⊢ trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)
  · simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]
  rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ ∀ {Z : PresheafedSpace C} (g h : Z ⟶ X.restrict hf), g ≫ X.ofRestrict hf = h ≫ X.ofRestrict hf → g = h

Tactic:
intro Z g₁ g₂ eq

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ g₁ = g₂
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
⊢ IsUnit f

Tactic:
choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x x.2 (h x.1 x.2)
  have hcover : U ≤ iSup V := by
    intro x hxU
    simp only [Opens.mem_iSup]
    tauto
  -- Let `g x` denote the inverse of `f` in `U x`.
  choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
  have ic : IsCompatible (sheaf X).obj V g := by
    intro x y
    apply section_ext X.sheaf (V x ⊓ V y)
    rintro z ⟨hzVx, hzVy⟩
    rw [germ_res_apply, germ_res_apply]
    apply (h z ((iVU x).le hzVx)).mul_right_inj.mp
    rw [← germ_res_apply X.presheaf (iVU x) z hzVx f]
    -- Porting note: change was not necessary in Lean3
    change X.presheaf.germ _ z hzVx _ * (X.presheaf.germ _ z hzVx _) =
      X.presheaf.germ _ z hzVx _ * X.presheaf.germ _ z hzVy (g y)
    rw [← map_mul, hg x, germ_res_apply X.presheaf _ _ _ f,
      ← germ_res_apply X.presheaf (iVU y) z hzVy f, ← map_mul, (hg y), map_one, map_one]
  -- We claim that these local inverses glue together to a global inverse of `f`.
  obtain ⟨gl, gl_spec, -⟩ :
    -- We need to rephrase the result from `ConcreteCategory` to `CommRingCat`.
    ∃ gl : X.presheaf.obj (op U), (∀ i, ((sheaf X).obj.map (iVU i).op) gl = g i) ∧ _ :=
    X.sheaf.existsUnique_gluing' V U iVU hcover g ic
  refine .of_mul_eq_one gl <| X.sheaf.eq_of_locally_eq' V U iVU hcover _ _ fun i ↦ ?_
  -- We need to rephrase the goal from `ConcreteCategory` to `CommRingCat`.
  change ((sheaf X).obj.map (iVU i).op).hom (f * gl) = ((sheaf X).obj.map (iVU i).op) 1
  rw [map_one, map_mul, gl_spec]
  exact hg i

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (CommRingCat.Hom.hom (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p)) 0
⊢ ∃ m, m • x = 0

Tactic:
toPushforwardStalk

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap (↑(CommRingCat.of ↑S))
              ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj (op ⊤)))) ≫
          ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
            ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
have := congr_app s.condition (op (opensFunctor f |>.obj x))

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
this :
  (s.fst ≫ f).c.app (op ((opensFunctor f).obj x)) =
    (s.snd ≫ g).c.app (op ((opensFunctor f).obj x)) ≫ s.pt.presheaf.map (eqToHom ⋯)
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
have e := (IsLocalization.algEquiv (.powers f) S
    (Localization.Away f)).symm.toAlgHom.comp_algebraMap

Goal state after:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥Y
hx : x ∉ Set.range ⇑f
⊢ x ∈ ⇑f '' X.zeroLocus s ↔ x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f

Tactic:
· simp only [Set.mem_inter_iff, hx, and_false, iff_false]
    exact fun H ↦ hx (Set.image_subset_range _ _ H)

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x✝ : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x✝ ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
Vb : Opens ↑(PrimeSpectrum.Top R)
mb : ↑x✝ ∈ Vb
ib : Vb ⟶ U
rb : M
sb : R
wb : ∀ (x : ↥Vb), ∃ (hs : sb ∉ (↑x).asIdeal), (fun x ↦ b (ib x)) x = LocalizedModule.mk rb ⟨sb, hs⟩
x : ↥(Va ⊓ Vb)
hsax : sa ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsa : (fun x ↦ a (ia x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk ra ⟨sa, hsax⟩
⊢ ∃ (hs : sa * sb ∉ (↑x).asIdeal),
    (fun x ↦ (a + b) ((Va.infLELeft Vb ≫ ia) x)) x = LocalizedModule.mk (sb • ra + sa • rb) ⟨sa * sb, hs⟩

Tactic:
obtain ⟨hsbx, hsb⟩ := wb ⟨x.1, x.2.2⟩

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x✝ : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x✝ ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
Vb : Opens ↑(PrimeSpectrum.Top R)
mb : ↑x✝ ∈ Vb
ib : Vb ⟶ U
rb : M
sb : R
wb : ∀ (x : ↥Vb), ∃ (hs : sb ∉ (↑x).asIdeal), (fun x ↦ b (ib x)) x = LocalizedModule.mk rb ⟨sb, hs⟩
x : ↥(Va ⊓ Vb)
hsax : sa ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsa : (fun x ↦ a (ia x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk ra ⟨sa, hsax⟩
hsbx : sb ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsb : (fun x ↦ b (ib x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk rb ⟨sb, hsbx⟩
⊢ ∃ (hs : sa * sb ∉ (↑x).asIdeal),
    (fun x ↦ (a + b) ((Va.infLELeft Vb ≫ ia) x)) x = LocalizedModule.mk (sb • ra + sa • rb) ⟨sa * sb, hs⟩