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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
this : ↑(RelSeries.snoc p y ⋯).length ≤ height (RelSeries.snoc p y ⋯).last
⊢ ↑p.length + 1 ≤ height y

Tactic:
simpa using this

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin ((mk (↑lf) f ⋯).length + 1)), (mk (↑lf) f ⋯).toFun i = (mk (↑lf) g ⋯).toFun i
⊢ f = g

Tactic:
mk_toFun lf f mf,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin ((mk (↑lf) f ⋯).length + 1)), f i = (mk (↑lf) g ⋯).toFun i
⊢ f = g
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
        obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
        apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ { length := l, toFun := f, step := mf } ∈ Finset.map (injStrictMono (Fintype.card α)) Finset.univ

Tactic:
simp_rw [Finset.mem_map, Finset.mem_univ, true_and, Subtype.exists]

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a, ∃ (b : StrictMono a.snd), (injStrictMono (Fintype.card α)) ⟨a, b⟩ = { length := l, toFun := f, step := mf }
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤

Tactic:
rw [RelSeries.last] at hlast
          simp [hlast]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsLeft R ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular ↑s

Tactic:
le_nonZeroDivisorsLeft_iff_isLeftRegular,

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ (∀ (s : ↥S), IsLeftRegular ↑s) ∧ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular ↑s
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : N ⊗[R] M
⊢ (rTensor M id) x = x

Tactic:
rTensor_id,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : N ⊗[R] M
⊢ id x = x
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1

Tactic:
simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H
    exact H.symm.imp (·.1.2) (·.2.2)

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

Goal state before:
pp: case refine_2
m n : ℕ
h : m = 1 ∨ n = 1
⊢ IsCoprime m n

Tactic:
· obtain rfl | rfl := h
    · exact isCoprime_one_left
    · exact isCoprime_one_right

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

Goal state before:
pp: case cons.mpr
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
⊢ ∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1

Tactic:
use fun i ↦ if i = a then u else v * μ i

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
⊢ ∑ i ∈ cons a t hat, (fun i ↦ if i = a then u else v * μ i) i * ∏ j ∈ cons a t hat \ {i}, s j = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ map₂ (LinearMap.mul R A) P (R ∙ y) ↔ ∃ z ∈ P, z * y = x

Tactic:
map₂_span_singleton_eq_map_flip,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ map ((LinearMap.mul R A).flip y) P ↔ ∃ z ∈ P, z * y = x
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) ↔ x ∈ J

Tactic:
exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
b : K
⊢ EuclideanDomain.gcd 0 b = b

Tactic:
by
  rw [Field.gcd_eq, if_pos rfl]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a

Tactic:
split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]

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

Goal state before:
pp: S : Type v
inst✝¹ : Semiring S
ι : Type u_3
R : ι → Type u_4
inst✝ : (i : ι) → Semiring (R i)
φ : (i : ι) → S →+* R i
⊢ ker (RingHom.pi φ) = ⨅ i, ker (φ i)

Tactic:
ext x
  simp [mem_ker, funext_iff]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
this : x * y ∣ z * gcd x y
⊢ x * y / gcd x y ∣ z

Tactic:
by
    obtain ⟨p, hp⟩ := this
    use p
    generalize gcd x y = g at hxy hs hp ⊢
    subst hs
    rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
    rw [← mul_assoc]
    simp only [mul_right_comm]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd 0 = normalize a * gcd 0

Tactic:
gcd_zero,

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ 0 = normalize a * 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated (gcd 0) (a * gcd 0)

Tactic:
gcd_zero,

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated 0 (a * 0)
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℕ
⊢ Associated (a.gcd b * a.lcm b) (a * b)

Tactic:
by rw [Nat.gcd_mul_lcm]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅

Tactic:
obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ⊔ Ideal.span {y} ≤ Ideal.span {z}

Tactic:
sup_le_iff

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ normalize a ∣ a

Tactic:
exact (normalize_associated _).dvd

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : a = 0
⊢ normalize b ∣ b

Tactic:
exact (normalize_associated _).dvd

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : {x | x ∈ S ∧ x ≠ 0}.Nonempty
wf : WellFounded EuclideanDomain.r
hmin : wf.min {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ wf.min {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
⊢ wf.min {x | x ∈ S ∧ x ≠ 0} h ∣ x % wf.min {x | x ∈ S ∧ x ≠ 0} h

Tactic:
have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∉
                    { x : R | x ∈ S ∧ x ≠ 0 } :=
                  fun h₁ => WellFounded.not_lt_min wf _ h₁ (mod_lt x hmin.2)

Goal state after:
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : {x | x ∈ S ∧ x ≠ 0}.Nonempty
wf : WellFounded EuclideanDomain.r
hmin : wf.min {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ wf.min {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : x % wf.min {x | x ∈ S ∧ x ≠ 0} h ∉ {x | x ∈ S ∧ x ≠ 0}
⊢ wf.min {x | x ∈ S ∧ x ≠ 0} h ∣ x % wf.min {x | x ∈ S ∧ x ≠ 0} h
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
f : α → α
hf : Function.Involutive f
x✝ : Matrix m n α
⊢ (fun M ↦ M.map f) ((fun M ↦ M.map f) x✝) = x✝

Tactic:
simp [hf]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ ↑(Fintype.card ι)

Tactic:
have : Nontrivial R := nontrivial_of_invariantBasisNumber R

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ι)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #ι ≤ #κ

Tactic:
have : Nontrivial R := nontrivial_of_invariantBasisNumber R

Goal state after:
case a
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
this : Nontrivial R
⊢ #ι ≤ #κ
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

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

Tactic:
by
  rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]
  · exact rank_top_le_rank_of_isScalarTower R S M
  · exact lt_of_le_of_lt (rank_top_le_rank_of_isScalarTower R S M) (Module.rank_lt_aleph0 R M)
  · exact Module.rank_lt_aleph0 _ _

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

Tactic:
by_cases h₁ : i = a

Goal state after:
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (∑ j_1, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = 0 a b

Tactic:
by_cases h₁ : i = a

Goal state after:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
⊢ (∑ j_1, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = 0 a b

case neg
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : ¬i = a
⊢ (∑ j_1, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = 0 a b
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
⊢ diagonal (fun x ↦ M i i) j j = M j j

Tactic:
diagonal_apply_eq

Goal state after:
case inr.inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
⊢ M i i = M j j
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a ≤ s.sup' hs fun i ↦ f i + a

Tactic:
apply add_le_of_le_tsub_right_of_le

Goal state after:
case a.h
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i ↦ f i + a

case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α * lift.{u, v} #β = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
mul_eq_max_of_aleph0_le_left

Goal state after:
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ max (lift.{v, u} #α) (lift.{u, v} #β) = max (lift.{v, u} #α) (lift.{u, v} #β)

case h
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ ℵ₀ ≤ lift.{v, u} #α

case h'
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≠ 0
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
apply mk_finsupp_lift_of_infinite

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
⊢ Nonempty (Unique ι)

Tactic:
have : Nontrivial R := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this : Nontrivial R
⊢ Nonempty (Unique ι)
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J

Tactic:
· let s : TwoSidedIdeal R := .mk'
      {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
      ⟨0, ⟨zero_mem _, ⟨0, ⟨zero_mem _, zero_add _⟩⟩⟩⟩
      (by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩)
      (by rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩)
    suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by
      intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl
    refine sup_le (fun x y h => ?_) (fun x y h => ?_) <;> rw [rel_iff] at h ⊢ <;> rw [mem_mk']
    exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Codisjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Codisjoint (toSubmodule S) (Submodule.restrictScalars R I)

Tactic:
by
  simp [← Submodule.codisjoint_restrictScalars_iff R]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
ι : Type v
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → Module R (δ i j)
r : R
⊢ ∀ (x : ⨁ (i : (x : ι) × α x), δ i.fst i.snd), (↑sigmaCurry).toFun (r • x) = (RingHom.id R) r • (↑sigmaCurry).toFun x

Tactic:
by convert! DFinsupp.sigmaCurry_smul (δ := δ) r

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✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : ⇑f ⁻¹' {0} ⊆ ↑S
⊢ comap f (map f S) = S

Tactic:
convert! comap_map_eq f S
  rwa [left_eq_sup, Algebra.adjoin_le_iff]

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

Goal state before:
pp: case inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun i ↦ diagonal fun j ↦ d i j) i₁ i₁ j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Tactic:
diagonal_apply_eq

Goal state after:
case inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ d i₁ j₁ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)

Tactic:
diagonal_apply_eq

Goal state after:
case inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ d i₁ j₁ = d (i₁, j₁).1 (i₁, j₁).2
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = diagonal (Function.update v i x) j j

Tactic:
diagonal_apply_eq

Goal state after:
case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j