mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i ≠ toInt val j ↔ val i ≠ val j

Tactic:
simpa using (toInt_eq_toInt val i j).not

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j

Tactic:
rw [mul_assoc]

Goal state after:
case cons.mp.refine_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
rw [mul_assoc]

Goal state after:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * (μ x * ((∏ j ∈ t \ {x}, s j) * s a))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = (fun x1 x2 ↦ x1 • x2) y (f i)

Tactic:
refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩

Goal state after:
case mp.refine_1.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
⊢ (Finsupp.single i y) j ∈ I

case mp.refine_1.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ ((Finsupp.single i y).sum fun i c ↦ c • f i) = (fun x1 x2 ↦ x1 • x2) y (f i)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ q, q.IsPrime ∧ comap f q = p

pp: case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p

Tactic:
· obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
      (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)
    exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
      (map_le_iff_le_comap.mp hq₂)⟩

Goal state after:
case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z

pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z

Tactic:
· rw [hxy, div_zero]
    rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
    rwa [hxy.1] at hxz

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ (∀ (a : M) (b : M'), x✝ • (a, b) = 0) ↔ (∀ (m : M), x✝ • m = 0) ∧ ∀ (m : M'), x✝ • m = 0

Tactic:
Prod.smul_mk,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ (∀ (a : M) (b : M'), (x✝ • a, x✝ • b) = 0) ↔ (∀ (m : M), x✝ • m = 0) ∧ ∀ (m : M'), x✝ • m = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * j * b ∈ I * J

Tactic:
rw [mul_assoc]

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * (j * b) ∈ I * J
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0

pp: case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0

Tactic:
· rw [hx, lcm_zero_left]

Goal state after:
case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0

pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : (i : ι) → M i), r • m = 0

Tactic:
· intro i m
    classical simpa using congr_fun (h (Pi.single i m)) i

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : (i : ι) → M i), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
⊢ (map f I).IsPrime

Tactic:
by
  have h : I.map f = I.map ((RingEquivClass.toRingEquiv f : R ≃+* S) : R →+* S) := rfl
  rw [h, map_comap_of_equiv (RingEquivClass.toRingEquiv f : R ≃+* S)]
  exact Ideal.IsPrime.comap (RingEquivClass.toRingEquiv f : R ≃+* S).symm

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0

Tactic:
constructor
  · intro h x hx
    apply eq_zero_of_zero_dvd
    rw [← h]
    apply gcd_dvd hx
  · refine s.induction_on ?_ ?_
    · simp
    intro a s sgcd h
    simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
by
  rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
  simp

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
by
  rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
  simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i

Tactic:
classical
    refine Finset.induction_on s ?_ ?_
    · grind [Submodule.mem_top]
    · grind [mul_mem_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : Group α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S

Tactic:
mem_nonunits_iff,

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : Group α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬IsUnit a ↔ (↑a)⁻¹ ∉ S
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ a ∈ nonunits ↥S ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S

Tactic:
mem_nonunits_iff,

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬IsUnit a ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ normalize (normalize x) = normalize x

Tactic:
by simp [normalize_apply]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
rw [gcd_eq_zero_iff] at hg
    rcases hg with ⟨rfl, rfl⟩
    exact
      (gcd_zero_left' (0 ^ k : α)).dvd.trans
        (pow_dvd_pow_of_dvd (gcd_zero_left' (0 : α)).symm.dvd _)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
← mul_dvd_mul_iff_left h,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ gcd a b * lcm a b ∣ gcd a b * c ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ (Multiset.map (fun x ↦ x) s.val).prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
Multiset.map_id'

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
by
  let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
  let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
  exact le_of_fin_injective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.injective.comp (i.comp P.injective))

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b : R
⊢ ∃ x y, gcd a b = a * x + b * y

Tactic:
by
  rw [← gcd_dvd_iff_exists]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
by
  obtain ⟨y, i, hmem, hi⟩ := Ideal.IsMaximal.exists_inv ‹_› hx
  obtain ⟨y, hy⟩ : ∃ y : R, y * x + i ^ n = 1 := by
    induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa
  exact ⟨y, i ^ n, Ideal.pow_mem_pow hmem n, hy⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
N : Submodule R M
⊢ Ideal.span s • N = s • N

Tactic:
← coe_set_smul,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
N : Submodule R M
⊢ ↑(Ideal.span s) • N = s • N
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ (b.smulTower c) ((Equiv.prodComm ι ι').symm ij) = b ij.2 • c ij.1

Tactic:
smulTower_apply

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ b ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g 0 = toMultiset (mapDomain g 0)

Tactic:
Multiset.map_zero,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ 0 = toMultiset (mapDomain g 0)
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
rw [iUnionLift_of_mem x (hik hi), iUnionLift_of_mem y (hjk hj), ← h k]

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = f k (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
by rw [le_def, le_def]; constructor <;> intro h _ _ h' <;> exact h h'

Goal state after:
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
by rw [le_def, le_def]; constructor <;> intro h _ _ h' <;> exact h h'

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: case pos
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : Module.Finite S M
this : Module.Finite R M
⊢ finrank S M ≤ finrank R M

Tactic:
exact finrank_top_le_finrank_of_isScalarTower R S M

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = Subsemiring.closure ↑S.toSubsemiring ⊔ T.toSubsemiring

Tactic:
← T.toSubsemiring.closure_eq,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = Subsemiring.closure ↑S.toSubsemiring ⊔ Subsemiring.closure ↑T.toSubsemiring
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
⊢ (A.submatrix ⇑e ⇑f).updateRow i r = (A.updateRow (e i) fun j ↦ r (f.symm j)).submatrix ⇑e ⇑f

Tactic:
ext i' j

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ (A.submatrix ⇑e ⇑f).updateRow i r i' j = (A.updateRow (e i) fun j ↦ r (f.symm j)).submatrix (⇑e) (⇑f) i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
i : m
a : α
⊢ vecMulVec (Function.update u i a) v = (vecMulVec u v).updateRow i (a • v)

Tactic:
ext i' j

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
⊢ vecMulVec (Function.update u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ baseChange A (span R s) = span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
rw [baseChange_eq_span, map_span, span_span_of_tower]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ (sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

Tactic:
simp_rw [← add_oreDiv, ← OreLocalization.expand']

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ r₁ /ₒ s₁ + (ra • r₂ /ₒ (sa * s₁) + rc • r₃ /ₒ (sc * (sa * s₁))) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
⊢ f m = 0 ↔ ∃ s, ↑s * m = 0

Tactic:
by
  simp_rw [← f.map_zero, eq_iff_exists, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ mk' S 0 (sec M x).2 = 0

Tactic:
mk'_zero

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : Subalgebra F E
h : K.toSubsemiring = K'.toSubsemiring
⊢ K = K'

Tactic:
rwa [SetLike.ext'_iff] at h ⊢

Goal state after:
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) * (algebraMap R Sₘ) ↑y = (algebraMap R Sₘ) x

Tactic:
IsScalarTower.algebraMap_apply R Rₘ Sₘ,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) * (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑y) = (algebraMap R Sₘ) x
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) * (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑y) = (algebraMap R Sₘ) x

Tactic:
IsScalarTower.algebraMap_apply R Rₘ Sₘ,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) * (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)