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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
    (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) →
      ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → p.length ≠ 0 → ↑p.length ≤ n
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ n

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ n

Tactic:
· simp_all

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x

Tactic:
· simp_all

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ (p.smash q h).last = q.last

Tactic:
by
  dsimp only [smash, last]
  rw [← Fin.natAdd_last, Fin.addCases_right]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ + 1 ≤ height b

Tactic:
have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
this : ⊤ ≤ height b
⊢ ⊤ + 1 ≤ height b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
· simp_all

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

Tactic:
obtain ⟨t, i, hi, ht⟩ := this (s.cons ⊥ (bot_lt_iff_ne_bot.mpr h₁)) rfl
    exact ⟨t, ⟨fun j ↦ i (j.succ.cast (by simp)), fun _ _ ↦ by simp⟩,
      funext fun j ↦ (congr_fun hi _).trans (RelSeries.cons_cast_succ _ _ _ _), ht⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
this : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], krullDim α < ⊤ → ↑(⨆ a, height a + coheight a) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

pp: α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
· simp_all

Goal state after:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x : M ⊗[R] N
p : M
q : N
⊢ (liftAux f') (r • p ⊗ₜ[R] q) = σ₁₂ r • (liftAux f') (p ⊗ₜ[R] q)

Tactic:
by simp_rw [← tmul_smul, liftAux_tmul, (f' p).map_smulₛₗ]

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

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • (x + y) = r • (x + y) + s • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]
    rw [ihx, ihy, add_add_add_comm]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.inr
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α)),
    RelSeries.last p = ↑x → p.length ≠ 0 → ↑p.length ≤ height x + 1
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

Tactic:
· simp_all

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ height x + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
⊢ False

Tactic:
let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩

Goal state after:
case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
⊢ False
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n✝ n : ℕ
⊢ (mulRight R a ^ n) ∘ₗ mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a

Tactic:
pow_mulRight

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n✝ n : ℕ
⊢ mulRight R (a ^ n) ∘ₗ mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_2.mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N

Tactic:
· simp_all

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ t • x
⊢ r • m ∈ (s * t) • x

Tactic:
have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
      obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
      rw [Finsupp.sum, AddSubmonoid.coe_finsetSum]
      simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]
      exact Submodule.sum_mem _ fun r' hr' ↦
        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_9
Q : Type u_10
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R P
inst✝ : Module R Q
p : Submodule R P
q : Submodule R Q
⊢ (map p.subtype q.subtype).range = Submodule.map₂ (mk R P Q) p q

Tactic:
range_map,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_9
Q : Type u_10
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R P
inst✝ : Module R Q
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ (mk R P Q) p.subtype.range q.subtype.range = Submodule.map₂ (mk R P Q) p q
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n ∈ ⊥
⊢ m • n ∈ ⊥

Tactic:
rw [AddSubmonoid.mem_bot] at hn ⊢

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n = 0
⊢ m • n = 0
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
by
    rw [add_le_iff] at this
    nth_rw 1 [← one_mul a∗]
    exact (mul_left_mono this.1).trans (mul_kstar_le_self this.2)

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this : List.Pairwise (fun a b ↦ decide (a ≤ b) = true) (li.mergeSort fun a b ↦ decide (a ≤ b))
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose] ↔ ↑hi.choose ≤ ↑hj.choose

Tactic:
rw [List.pairwise_iff_get] at this

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose] ↔ ↑hi.choose ≤ ↑hj.choose
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R N} [∀ (i : β), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
intro _ _ e h _ _

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
α✝ β✝ : Type u_6
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R N
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
⊢ map (Pi.evalRingHom R i) (pi I) = I i

Tactic:
by
  ext r
  rw [mem_map_iff_of_surjective (Pi.evalRingHom R i) (Function.surjective_eval _)]
  classical refine ⟨?_, fun hr ↦ ⟨_, single_mem_pi hr, by simp⟩⟩
  rintro ⟨r, hr, rfl⟩
  exact hr i

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd

Tactic:
refine s.induction_on ?_ fun b s ih ↦ ?_
  · simp_rw [map_zero, gcd_zero, mul_zero]
  · simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
    rw [ih]
    apply ((normalize_associated a).mul_right _).gcd_eq_right

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

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

pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a b * gcd a (b ^ k) ∣ gcd a b * gcd a b ^ k

Tactic:
· exact gcd_mul_dvd_mul_gcd a b (b ^ k)

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a b * gcd a (b ^ k) ∣ gcd a b * gcd a b ^ k
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
f : Multiset α
hf : factors a = b ::ₘ f
⊢ (b ::ₘ f).card = 1

Tactic:
card_cons,

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
⊢ f.card + 1 = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

Tactic:
simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Ideal R
inst✝ : IsPrincipal S
is_prime : S.IsPrime
ne_bot : S ≠ ⊥
x✝¹ x✝ : R
⊢ generator S ∣ x✝¹ * x✝ → generator S ∣ x✝¹ ∨ generator S ∣ x✝

Tactic:
simpa only [← mem_iff_generator_dvd S] using is_prime.2

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (if i✝ = j✝ then d i✝ else 0) ∈ S

Tactic:
ite_mem

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (i✝ = j✝ → d i✝ ∈ S) ∧ (¬i✝ = j✝ → 0 ∈ S)
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 w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k ↦ v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
w' : Finite ↑(Φ ⁻¹' {s})
⊢ False

Tactic:
exact w.false

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 ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ι)

Tactic:
Fintype.card_congr (Equiv.ofInjective b b.injective)

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 ↑(range ⇑b))
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 w
inst✝ : Fintype ι
h : Basis ι R M
this : Nontrivial R
⊢ ↑(Fintype.card ↑(range ⇑h)) = ↑(Fintype.card ι)

Tactic:
Set.card_range_of_injective h.injective

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
this : Nontrivial R
⊢ ↑(Fintype.card ι) = ↑(Fintype.card ι)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ finrank R S = 1

Tactic:
← (AlgEquiv.ofBijective (Algebra.ofId R S) h).toLinearEquiv.finrank_eq,

Goal state after:
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ finrank R R = 1
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✝ : α
a : m
b : n
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
by_cases hi : i = a <;> by_cases hj : j = b

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : i = a
hj : j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

case neg
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : i = a
hj : ¬j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

case pos
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : ¬i = a
hj : j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

case neg
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : ¬i = a
hj : ¬j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b
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 α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (if i = i✝ ∧ j = j✝ then a else 0) ∈ S

Tactic:
ite_mem

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (i = i✝ ∧ j = j✝ → a ∈ S) ∧ (¬(i = i✝ ∧ j = j✝) → 0 ∈ S)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
⊢ Aᵀ *ᵥ x = x ᵥ* A

Tactic:
ext
  apply dotProduct_comm

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
⊢ x ᵥ* Aᵀ = A *ᵥ x

Tactic:
ext
  apply dotProduct_comm

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommMagma α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
⊢ (M * N)ᵀ = Nᵀ * Mᵀ

Tactic:
ext
  apply dotProduct_comm

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ 1 = prod 0 fun a n ↦ a ^ n

Tactic:
Finsupp.prod_zero_index

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A)

Tactic:
lift_umax.{v, w}

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A)
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (lift.{w, v} (Module.rank F K)) * toNat (lift.{v, w} (Module.rank K A)) = toNat (Module.rank F A)

Tactic:
← toNat_mul,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A)) = toNat (Module.rank F A)
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (DirectSum.id M ι) x = x default

Tactic:
rw [← AddEquiv.eq_symm_apply, id_symm_apply, eq_comm]
  induction x using DirectSum.induction_on <;> simp [Unique.eq_default, *]

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

Goal state before:
pp: case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]
  exact Function.Bijective.surjective h

Goal state after: