mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ WfDvdMonoid α

Tactic:
have : WellFounded (α := {I : Ideal α // I.IsPrincipal}) (· > ·) := h

Goal state after:
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
⊢ WfDvdMonoid α
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a ≠ 0
b : α
hb : b ∈ factors a
⊢ (factors a).card = 1

Tactic:
obtain ⟨f, hf⟩ := exists_cons_of_mem hb

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
⊢ (factors a).card = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
Finset.prod_eq_multiset_prod,

Goal state after:
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
Module: Mathlib.GroupTheory.DedekindFinite

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
a b : M
hab : a * b = 1
⊢ b * a = 1

Tactic:
by
    have ⟨c, hbc⟩ := Finite.surjective_of_injective (isLeftRegular_of_mul_eq_one hab) 1
    rwa [left_inv_eq_right_inv hab hbc]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ { s // LinearIndepOn R id s }

Tactic:
exact
        ⟨Set.range v, by
          rw [LinearIndepOn]
          convert! v.reindexRange.linearIndependent
          simp⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ Nontrivial M

Tactic:
← not_subsingleton_iff_nontrivial

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ ¬Subsingleton M
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ Module.rank R M = 1

Tactic:
rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_toSpanSingleton h]

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ ∑ x, ∑ i ∈ s, u x * v i x = ∑ i ∈ s, ∑ i_1, u i_1 * v i i_1

Tactic:
Finset.sum_comm

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ ∑ y ∈ s, ∑ x, u x * v y x = ∑ i ∈ s, ∑ i_1, u i_1 * v i i_1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
⊢ ∑ x, ∑ i ∈ s, u i x * v x = ∑ i ∈ s, ∑ i_1, u i i_1 * v i_1

Tactic:
Finset.sum_comm

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
⊢ ∑ y ∈ s, ∑ x, u y x * v x = ∑ i ∈ s, ∑ i_1, u i i_1 * v i_1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x ∈ s, I ≤ f x
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
refine ⟨aux, fun ⟨i, his, hi⟩ ↦ Set.Subset.trans hi ?_⟩

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x ∈ s, I ≤ f x
x✝ : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ ↑(f i) ⊆ ⋃ i ∈ ↑s, ↑(f i)
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 : R
hmem : i ∈ I
hi : y✝ * x + i = 1
y : R
hy : y * x + i ^ n = 1
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
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✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
⊢ ∀ m ∈ { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I,
    ∀ n ∈ M, m * n ∈ I • M

Tactic:
rintro _ ⟨r, hr, rfl⟩ a ha; rw [Algebra.linearMap_apply, ← Algebra.smul_def]
    exact Submodule.smul_mem_smul hr ha

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
hs : s ⊆ ↑(I ⊔ J).radical
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical

Tactic:
by
  replace hs : ∀ z : s, ∃ (m : ℕ) (a b : R) (ha : a ∈ I) (hb : b ∈ J), a + b = z ^ m := by
    rintro ⟨z, hzs⟩
    simp only [Ideal.radical, Submodule.mem_sup] at hs
    obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
    exact ⟨m, y, b, hyq, hb, hy⟩
  choose m a b ha hb heq using hs
  refine ⟨a, by rwa [Set.range_subset_iff], fun z hz ↦ ⟨m ⟨z, hz⟩, heq ⟨z, hz⟩ ▸ ?_⟩⟩
  exact Ideal.add_mem _ (mem_sup_left (subset_span ⟨⟨z, hz⟩, rfl⟩)) (mem_sup_right <| hb _)

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ : C →ₐ[A] D
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := f, map_one' := map_one'✝¹ }.toFun x * { toFun := f, map_one' := map_one'✝¹ }.toFun y
map_zero'✝¹ : (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun x +
        (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun y
commutes'✝ :
  ∀ (r : A),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap A B) r) =
      (algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := g, map_one' := map_one'✝ }.toFun x * { toFun := g, map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
hg :
  ∀ (r : B),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap B C) r) =
      (algebraMap B D) r
⊢ f = fun x ↦ g ((algebraMap B C) x)

Tactic:
ext x
      exact (hg x).symm

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
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⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)
  have : ci i = ⟨c, hi⟩ := Subtype.ext (hci i)
  rw [iUnionLift_of_mem _ hi, ← this, h]

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ 0 • {a} = 0

Tactic:
apply zero_nsmul

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x✝ : m
⊢ ∑ x_1, ∑ i ∈ s, x i x✝ x_1 * y x_1 = ∑ c ∈ s, ∑ x_1, x c x✝ x_1 * y x_1

Tactic:
Finset.sum_comm

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x✝ : m
⊢ ∑ y_1 ∈ s, ∑ x_1, x y_1 x✝ x_1 * y x_1 = ∑ c ∈ s, ∑ x_1, x c x✝ x_1 * y x_1
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x✝ : m
⊢ ∑ x_1, ∑ i ∈ s, x x_1 * y i x_1 x✝ = ∑ c ∈ s, ∑ x_1, x x_1 * y c x_1 x✝

Tactic:
Finset.sum_comm

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x✝ : m
⊢ ∑ y_1 ∈ s, ∑ x_1, x x_1 * y y_1 x_1 x✝ = ∑ c ∈ s, ∑ x_1, x x_1 * y c x_1 x✝
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 0 ∈ s

Tactic:
by simpa using h.2.2 0

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
⊢ ∀ {a b : S}, a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
intro a b ⟨m, hm, ha⟩ ⟨n, hn, hb⟩
    refine ⟨_, mul_mem hn hm, ?_⟩
    rw [mul_add, mul_assoc, mul_comm n m, mul_assoc]
    exact add_mem (mul_mem (H hn) ha) (mul_mem (H hm) hb)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝¹ x✝ : Subalgebra R A
⊢ x✝¹.toNonUnitalSubalgebra = x✝.toNonUnitalSubalgebra → x✝¹ = x✝

Tactic:
by simp [SetLike.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case mem
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : x ∈ adjoin R s
z : A
hz : z ∈ s
⊢ p x z hx ⋯

Tactic:
| mem z hz =>

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

Goal state before:
pp: case mem
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
hx : x ∈ adjoin R s
z : A
hz : z ∈ s
⊢ p x z hx ⋯

Tactic:
| mem z hz =>

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * y ∈ span R ↑(Subsemigroup.closure s)
hyz : x * z ∈ span R ↑(Subsemigroup.closure s)
⊢ x * (y + z) ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_add] using add_mem hxz hyz

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ 0 = 0

Tactic:
exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
by
  subst hT
  dsimp [iSupLift]
  apply Set.iUnionLift_of_mem

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A →ₐ[R] B
x : A
⊢ Subalgebra.map e R[x] = R[e x]

Tactic:
rw [map_adjoin, Set.image_singleton]

Goal state after:
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g p

Tactic:
conv_rhs => rw [← hs p]

Goal state after:
case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g ((linearCombination R id) (s p))
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
f g : A ≃⋆ₐ[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by
    rcases f with ⟨⟨⟨⟨_, _, _⟩, _⟩, _⟩, _⟩
    rcases g with ⟨⟨⟨⟨_, _, _⟩, _⟩, _⟩, _⟩
    congr

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (-f))) 1) x✝ = ((AlgebraTensorModule.curry (-baseChange A f)) 1) x✝

Tactic:
simp [tmul_neg]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ False

Tactic:
obtain ⟨n, -, hn⟩ := Submonoid.mem_closure_finset (x := b).mp (by rw [hSgen]; exact mem_top _)

Goal state after:
case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ False
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 0 = 0

Tactic:
induction x using OreLocalization.ind with | _ r s
    rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']

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

Goal state before:
pp: 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
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
⊢ add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
simp only [add'']
  have ha := ore_eq (s₁ : R) s₂
  generalize oreNum (s₁ : R) s₂ = ra at *
  generalize oreDenom (s₁ : R) s₂ = sa at *
  rw [oreDiv_eq_iff]
  rcases oreCondition sb sa with ⟨rc, sc, hc⟩
  have : sc * rb * s₂ = rc * ra * s₂ := by
    rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
  rcases ore_right_cancel _ _ s₂ this with ⟨sd, hd⟩
  use sd * sc
  use sd * rc
  simp only [smul_add, smul_smul, Submonoid.smul_def, Submonoid.coe_mul]
  constructor
  · rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
  · rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ Function.Injective ⇑(Fintype.linearCombination R M.row)

Tactic:
congr! 1

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ ⇑M.vecMulLinear = ⇑(Fintype.linearCombination R M.row)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: case neg
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
⊢ nx / dx + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
by_cases hy0 : dy = 0

Goal state after:
case pos
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : dy = 0
⊢ nx / dx + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

case neg
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : ¬dy = 0
⊢ nx / dx + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
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
s : ↥S
⊢ f.mk' 0 s = 0

Tactic:
eq_comm,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
s : ↥S
⊢ 0 = f.mk' 0 s