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

Goal state before:
pp: case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)

Tactic:
rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]

Goal state after:
case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ∈ nonZeroDivisors S
⊢ x * y ∈ x • p ↔ y ∈ p

Tactic:
simp [mem_smul_pointwise_iff_exists, mul_cancel_left_mem_nonZeroDivisors hx]

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

Goal state before:
pp: case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx

Tactic:
simp_rw [pow_succ']

Goal state after:
case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M * M ^ n), C (n + 1) x ⋯
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submodule R N
⊢ IsNoetherian R N ↔ IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
  apply isNoetherian_of_range_eq_ker S.subtype S.mkQ
  rw [Submodule.ker_mkQ, Submodule.range_subtype]

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

Goal state before:
pp: case neg.h₁
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
⊢ x * y ∣ z * (x * gcdA x y)

pp: case h₂
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
⊢ x * y ∣ z * (y * gcdB x y)

Tactic:
· rw [mul_left_comm]
    gcongr
    apply hyz.mul_right

Goal state after:
case h₂
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
⊢ x * y ∣ z * (y * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)

Tactic:
intro y

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
⊢ y ∈ sInf (map f '' A) → y ∈ map f (sInf A)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
by_cases! h : ∀ x ∈ s, x = (0 : α)

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ f x * a) = s.gcd f * normalize a

Tactic:
by
  simp_rw [mul_comm]; exact gcd_mul_left

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ s.gcd f

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [gcd_cons, ← Int.coe_gcd]
    grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
by
  cases subsingleton_or_nontrivial α
  · use 0
    rw [Subsingleton.elim a (0 ^ k)]
  by_cases ha : a = 0
  · use 0
    obtain rfl | hk := eq_or_ne k 0
    · simp [ha] at h
    · rw [ha, zero_pow hk]
  by_cases hb : b = 0
  · use 1
    rw [one_pow]
    apply (associated_one_iff_isUnit.mpr hab).symm.trans
    rw [hb]
    exact gcd_zero_right' a
  obtain rfl | hk := k.eq_zero_or_pos
  · use 1
    rw [pow_zero] at h ⊢
    use Units.mkOfMulEqOne _ _ h
    rw [Units.val_mkOfMulEqOne, one_mul]
  have hc : c ∣ a * b := by
    rw [h]
    exact dvd_pow_self _ hk.ne'
  obtain ⟨d₁, d₂, hd₁, hd₂, hc⟩ := exists_dvd_and_dvd_of_dvd_mul hc
  use d₁
  obtain ⟨h0₁, ⟨a', ha'⟩⟩ := pow_dvd_of_mul_eq_pow ha hab h hc hd₁
  rw [mul_comm] at h hc
  rw [(gcd_comm' a b).isUnit_iff] at hab
  obtain ⟨h0₂, ⟨b', hb'⟩⟩ := pow_dvd_of_mul_eq_pow hb hab h hc hd₂
  rw [ha', hb', hc, mul_pow] at h
  have h' : a' * b' = 1 := by
    apply (mul_right_inj' h0₁).mp
    rw [mul_one]
    apply (mul_right_inj' h0₂).mp
    rw [← h]
    rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
  use Units.mkOfMulEqOne _ _ h'
  rw [Units.val_mkOfMulEqOne, ha']

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

Goal state before:
pp: case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b

Tactic:
rcases h with ⟨d, hd⟩
    rcases gcd_dvd_right a c with ⟨e, he⟩
    rcases gcd_dvd_left a c with ⟨f, hf⟩
    use e + f * d
    rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose ⋯ = a * 0
⊢ gcd a 0 ≠ 0

Tactic:
contrapose a0

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
h : gcd a 0 * Classical.choose ⋯ = a * 0
a0 : gcd a 0 = 0
⊢ a = 0
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), (A + b) i j = 0 i j) ∧ ∀ (i : m) (j : n), (b + A) i j = 0 i j) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0

Tactic:
add_apply,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), A i j + b i j = 0 i j) ∧ ∀ (i : m) (j : n), b i j + A i j = 0 i j) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0
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✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
⊢ ↑(finrank R M) = #ι

Tactic:
cases @nonempty_fintype _ (Module.Finite.finite_basis h)
  rw [Cardinal.mk_fintype, finrank_eq_card_basis h]

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
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
have := Module.rank_lt_aleph0 R M
  rw [← not_le] at this
  simp [Module.finrank, this, Module.rank_zero_iff_of_free]

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

Goal state before:
pp: case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑∅, ↑(f i)
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty] at h
        exact (h I.zero_mem).elim

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a : α
⊢ (single i j a)ᵀ = single j i a

Tactic:
by
  aesop (add unsafe unfold single)

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
i : m
j : n
a : α
β : Type u_10
inst✝² : Zero β
F : Type u_11
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
f : F
⊢ (single i j a).map ⇑f = single i j (f a)

Tactic:
by
  aesop (add unsafe unfold single)

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
⊢ (single i i c).diag j = Pi.single i c j

Tactic:
by_cases hij : i = j <;> (try rw [hij])

Goal state after:
case pos
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single j j c).diag j = Pi.single j c j

case neg
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : ¬i = j
⊢ (single i i c).diag j = Pi.single i c j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I * ⊤

Tactic:
by rw [mul_top, h]

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

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Finite n
inst✝² : Semiring R
i : m
j : n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ (stdBasis R m n) (i, j) = single i j 1

Tactic:
by
  simp [stdBasis, single_eq_of_single_single]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ ∀ x ∈ s, a = x

Tactic:
intro y

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
⊢ y ∈ s → a = y
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
⊢ ((∑ i ∈ s, x i) *ᵥ y) x✝ = (∑ i ∈ s, x i *ᵥ y) x✝

Tactic:
simp only [mulVec, dotProduct, sum_apply, Finset.sum_mul, Finset.sum_apply]

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
⊢ ∑ x_1, ∑ i ∈ s, x i x✝ x_1 * y x_1 = ∑ c ∈ s, ∑ x_1, x c x✝ x_1 * y x_1
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

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

Tactic:
by
  constructor
  · 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 _⟩⟩⟩⟩]
  · rintro ⟨y, ⟨hy, ⟨z, ⟨hz, rfl⟩⟩⟩⟩; exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.toSubring.subtype.range = S.toSubring

Tactic:
Subring.range_subtype

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.toSubring = S.toSubring
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)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → r • x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Projective R P

Tactic:
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)

Goal state after:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Function.LeftInverse ⇑(linearCombination R id) ⇑((b.constr ℕ) fun i ↦ Finsupp.single (b i) 1)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (if h : ji = ii then M ji jx (cast ⋯ ix) else 0) = if h : ii = ji then M ii (cast ⋯ jx) ix else 0

Tactic:
split_ifs <;> grind

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

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (map (f₁ + f₂) g) (x✝¹ ⊗ₜ[R] x✝) = (map f₁ g + map f₂ g) (x✝¹ ⊗ₜ[R] x✝)

Tactic:
add_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (map (f₁ + f₂) g) (x✝¹ ⊗ₜ[R] x✝) = (map f₁ g) (x✝¹ ⊗ₜ[R] x✝) + (map f₂ g) (x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (f₁ + f₂) x✝¹ ⊗ₜ[R] g x✝ = f₁ x✝¹ ⊗ₜ[R] g x✝ + f₂ x✝¹ ⊗ₜ[R] g x✝

Tactic:
add_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (f₁ x✝¹ + f₂ x✝¹) ⊗ₜ[R] g x✝ = f₁ x✝¹ ⊗ₜ[R] g x✝ + f₂ x✝¹ ⊗ₜ[R] g x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (map f (g₁ + g₂)) (x✝¹ ⊗ₜ[R] x✝) = (map f g₁ + map f g₂) (x✝¹ ⊗ₜ[R] x✝)

Tactic:
add_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (map f (g₁ + g₂)) (x✝¹ ⊗ₜ[R] x✝) = (map f g₁) (x✝¹ ⊗ₜ[R] x✝) + (map f g₂) (x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ f x✝¹ ⊗ₜ[R] (g₁ + g₂) x✝ = f x✝¹ ⊗ₜ[R] g₁ x✝ + f x✝¹ ⊗ₜ[R] g₂ x✝

Tactic:
add_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ f x✝¹ ⊗ₜ[R] (g₁ x✝ + g₂ x✝) = f x✝¹ ⊗ₜ[R] g₁ x✝ + f x✝¹ ⊗ₜ[R] g₂ x✝
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 n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
⊢ False

Tactic:
match hr : m r + n r with
  -- If that power is `0`, then `r` can be written as a product of elements of `S \ {r}` and `S` was
  -- not minimal. Contradiction.
  | 0 =>
    have : ({r} : Set M) ⊆ closure (S \ {r}) := by
      simp only [hr, pow_zero, one_mul] at hr'
      rw [hr', Set.singleton_subset_iff]
      refine mul_mem ?_ ?_ <;> refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _ <;>
        rw [← hr'] <;> simpa using hs
    specialize hSmax (y := S \ {r}) (by simp [Submonoid.closure_sdiff_eq_closure this, hSgen])
      Finset.sdiff_subset
    simpa using hSmax hrS
  -- Assume that power is `1`.
  | 1 =>
    -- By cancelling on both sides we get `∏ s ∈ S \ {r}, s ^ (m s + n s) = 1`.
    simp only [hr, pow_one, mul_assoc, eq_comm (a := r), mul_eq_left, LeftCancelMonoid.mul_eq_one,
      Finset.prod_eq_one_iff] at hr'
    -- Since `M` has a single unit, this means that
    -- `∏ s ∈ S \ {r}, s ^ m s = ∏ s ∈ S \ {r}, s ^ n s = 1`.
    -- Furthermore, `m r + n r = 1` implies that one of `m r` or `n r` is zero.
    -- Therefore one of `a` or `b` is `1`, contradicting the fact that they are non-units.
    obtain h | h : m r = 0 ∨ n r = 0 := by lia
    · obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
      simp at ha
    · obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
      simp at hb
  -- If that power is at least `2`, then we can write `1` as `r` times something.
  -- Since `M` has a single unit, this means that `r = 1`. Contradiction.
  | N + 2 => simp [hr, hr₀, pow_add, mul_assoc, mul_left_comm] at hr'

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
⊢ Subsingleton (OreLocalization S R) ↔ 0 ∈ S

Tactic:
by
  rw [← subsingleton_iff_zero_eq_one, OreLocalization.one_def,
    OreLocalization.zero_def, oreDiv_eq_iff]
  simp

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

Goal state before:
pp: case h.right
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
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * (↑sc * (sb * ↑s₁)) = ↑sd * rc * (↑sa * ↑s₁)

Tactic:
← mul_assoc (sc : R),

Goal state after:
case h.right
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
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * (↑sc * sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)