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

Goal state before:
pp: case mp
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
i : Fin (p.length + (singleton r newLast).length + 1 + 1)
⊢ (∃ y, p.toFun y = (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) i) ∨
    (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) i = newLast

Tactic:
exact Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
      (Fin.append_left _ _ _).symm⟩) i

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
i : Fin q.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i.castSucc) = q.toFun i.castSucc

Tactic:
apply Fin.addCases_right

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
i : Fin q.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i.succ) = q.toFun i.succ

Tactic:
apply Fin.addCases_right

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).head = p.toFun i

Tactic:
by
  simp [drop, head]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
hl : i < j
⊢ False

Tactic:
exact absurd he (s.strictMono hl).ne

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
h : (Algebra.lmul R A) a₁ = (Algebra.lmul R A) a₂
⊢ a₁ = a₂

Tactic:
by simpa using DFunLike.congr_fun h 1

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ (f a)∗

Tactic:
exact one_le_kstar

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y

Tactic:
let ⟨a, b, H⟩ := H1

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
⊢ x ∣ z

Tactic:
let ⟨a, b, H⟩ := H1

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ z
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
⊢ I.prod J = ⊤ ↔ I = ⊤ ∧ J = ⊤

Tactic:
rw [← prod_inj, prod_top_top]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
r : S
x : M
r_in : r ∈ s
x_in : x ∈ restrictScalars S N
⊢ r • x ∈ restrictScalars S (⇑(algebraMap S R) '' s • N)

Tactic:
rw [restrictScalars_mem, ← algebraMap_smul R r]
    exact mem_set_smul_of_mem_mem (Set.mem_image_of_mem _ r_in) x_in

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0

Tactic:
← injective_iff_map_eq_zero f,

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ Function.Injective ⇑f
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm 0 x = 0

Tactic:
by rw [lcm, zero_mul, zero_div]

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

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
obtain ⟨k1, rfl⟩ := hac

Goal state after:
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ (if a * ↑u = 0 then 1 else Exists.choose ⋯) = u⁻¹ * if a = 0 then 1 else Exists.choose ⋯

Tactic:
simp_rw [Units.mul_left_eq_zero, if_neg ha, eq_inv_mul_iff_mul_eq, ← Units.val_inj]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ ↑(u * Exists.choose ⋯) = ↑(Exists.choose ⋯)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · simp only [zero_mul, gcd_zero_left']
  obtain ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
  apply associated_of_dvd_dvd
  · rw [eq]
    gcongr
    exact
      dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
        ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)
  · exact dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
⊢ ⊥.IsRadical

Tactic:
rwa [isRadical_bot_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
← UniqueFactorizationMonoid.irreducible_iff_prime

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
by
  simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]
  apply WfDvdMonoid.exists_factors a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)
⊢ P a

Tactic:
← UniqueFactorizationMonoid.irreducible_iff_prime

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
⊢ P a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = c ^ k
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a

Tactic:
hc,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = (d₂ * d₁) ^ k
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
b_norm : NormalizationMonoid α
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }

Tactic:
cases Subsingleton.elim a_norm b_norm

Goal state after:
case refl.refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : StrongNormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
b_norm : StrongNormalizationMonoid α
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toStrongNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }

Tactic:
cases Subsingleton.elim a_norm b_norm

Goal state after:
case refl.refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : StrongNormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if a * b = 0 then 1 else Classical.choose ⋯) =
    (if a = 0 then 1 else Classical.choose ⋯) * if b = 0 then 1 else Classical.choose ⋯

Tactic:
simp_rw [if_neg (mul_ne_zero ha hb), if_neg ha, if_neg hb, Units.ext_iff, Units.val_mul]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ↑(Classical.choose ⋯) = ↑(Classical.choose ⋯) * ↑(Classical.choose ⋯)
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

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

Tactic:
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card α ≤ Fintype.card β
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card β ≤ Fintype.card α
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
let := IsBezout.toGCDDomain R
  exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h

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
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Fintype ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
have := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Fintype ι
this : Finite ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoidWithZero α
x✝ : IsGCDMonoid α ∧ Nonempty (StrongNormalizationMonoid α)
a✝ : GCDMonoid α
val✝ : StrongNormalizationMonoid α
⊢ Nonempty (StrongNormalizedGCDMonoid α)

Tactic:
by classical exact
    ⟨strongNormalizedGCDMonoidOfExistsGCD fun _ _ ↦ ⟨_, fun _ ↦ (dvd_gcd_iff ..).symm⟩⟩

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✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Finite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Finite ι
val✝ : Fintype ι
⊢ #ι ≤ ↑(Fintype.card ↑w)
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
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
cases fintypeOrInfinite J

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ #↑(range ⇑v) ≤ #↑J

case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
⊢ #↑(range ⇑v) ≤ #↑J
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
κ : Type w
v : κ → M
i : LinearIndependent R v
⊢ #κ ≤ #ι

Tactic:
classical
  -- We split into cases depending on whether `ι` is infinite.
  cases fintypeOrInfinite ι
  · rw [Cardinal.mk_fintype ι] -- When `ι` is finite, we have `linearIndependent_le_span`,
    have : Nontrivial R := nontrivial_of_invariantBasisNumber R
    rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]
    exact linearIndependent_le_span v i (range b) b.span_eq
  · -- and otherwise we have `linearIndependent_le_infinite_basis`.
    exact linearIndependent_le_infinite_basis b v i

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

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

Tactic:
by_cases h₁ : i = i''

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

case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
⊢ Module.Finite R M

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Module.Finite R M
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
t : Finset κ
inst✝ : OrderBot M
hs : s.Nonempty
ht : t.Nonempty
f : ι → M
g : κ → M
⊢ s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2

Tactic:
by
  simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]

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
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M

Tactic:
by
  rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]
  exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M),
    fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : StarAddMonoid R
x : R
inst✝ : IsStarNormal x
⊢ star (-x) * -x = -x * star (-x)

Tactic:
simp_rw [star_neg, neg_mul_neg, star_comm_self']

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

Goal state before:
pp: m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
simp [diagonal_apply_ne d this]

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

Goal state before:
pp: case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i ↦ d (i, k)) i i

Tactic:
blockDiag_apply,

Goal state after:
case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ diagonal d (i, k) (i, k) = diagonal (fun i ↦ d (i, k)) i i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j

Tactic:
blockDiag_apply,

Goal state after:
case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ diagonal d (i, k) (j, k) = diagonal (fun i ↦ d (i, k)) i j
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
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Star A
inst✝ : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ f.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
simp_rw [Algebra.algebraMap_eq_smul_one', map_smul']; simp

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

Goal state before:
pp: case «0».«0»
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply, Fin.sum_univ_succ]

Goal state after: