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

Goal state before:
pp: case mp
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : hu.choose * x + hv.choose * y = 1
⊢ IsCoprime x y

Tactic:
exact ⟨_, _, h1⟩

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
⊢ (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0

Tactic:
split_ifs with h1 <;> simp [h, h1]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y * ↑(normUnit x * normUnit y) = x * ↑(normUnit x) * (y * ↑(normUnit y))

Tactic:
ac_rfl

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

Goal state before:
pp: case cons
ι : Type u_1
s✝ : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ (cons a s has).gcd f

Tactic:
rw [gcd_cons, ← Int.coe_gcd]
    grind

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

Goal state before:
pp: case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ gcd a b ^ 0

Tactic:
pow_zero

Goal state after:
case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = c ^ 0
⊢ Associated (1 ^ 0) a

Tactic:
pow_zero

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
⊢ Associated 1 a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ f a * x * ↑u + (∑ a ∈ s, f a * g a) * y * ↑u =
    f a * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) a +
      ∑ x_1 ∈ s, f x_1 * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) x_1

Tactic:
simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∑ x ∈ s, f x * (g x * (y * ↑u)) = ∑ x_1 ∈ s, f x_1 * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) x_1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f

Goal state after:
case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
f : ι →₀ R
⊢ ∀ ⦃a₂ : ι →₀ R⦄,
    (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) a₂ →
      f = a₂
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f

Goal state after:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f : ι →₀ R
⊢ ∀ ⦃a₂ : ι →₀ R⦄,
    (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) a₂ →
      f = a₂
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
M : Matrix l m α
x : m → α
y : n → α
i✝ : l
j✝ : n
⊢ ∑ j, M i✝ j * (x j * y j✝) = (∑ x_1, M i✝ x_1 * x x_1) * y j✝

Tactic:
Finset.sum_mul,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
M : Matrix l m α
x : m → α
y : n → α
i✝ : l
j✝ : n
⊢ ∑ j, M i✝ j * (x j * y j✝) = ∑ i, M i✝ i * x i * y j✝
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: 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
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
cases isEmpty_or_nonempty n
  · exact ⟨0, Subsingleton.elim _ _⟩
  obtain ⟨i⟩ := ‹Nonempty n›
  refine ⟨M i i, Matrix.ext fun j k => ?_⟩
  simp only [scalar_apply]
  obtain rfl | hkl := Decidable.eq_or_ne j k
  · rw [diagonal_apply_eq]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rfl
    · exact diag_eq_of_commute_single (hM hij)
  · rw [diagonal_apply_ne _ hkl]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [col_eq_zero_of_commute_single (hM hkl.symm) hkl]
    · rw [row_eq_zero_of_commute_single (hM hij) hkl.symm]

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

Goal state before:
pp: n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
v w : n → R
⊢ f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w

Tactic:
simp only [dotProduct, map_sum f, f.map_mul, Function.comp]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
⊢ ↑((equivNatSumOfFintype α n).symm ⟨P, hP⟩) = ∑ a, ↑⟨P, hP⟩ a • {a}

Tactic:
change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
⊢ Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = (Multiset.map (fun a ↦ ↑⟨P, hP⟩ a • {a}) univ.val).sum
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a - b + (c - d) ∈ carrier

Tactic:
exact add_mem h1 h2

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
k : ι
⊢ k = i ∨ k = j

Tactic:
by simpa using Set.ext_iff.mp h k

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
⊢ (IsInternal fun i ↦ A ↑i) ↔ IsInternal A

Tactic:
simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

Tactic:
rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]
  congr 1 with z; simp [Submonoid.closure_union, Submonoid.mem_sup, Set.mem_mul]

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
⊢ S = S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
left_eq_sup,

Goal state after:
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
⊢ adjoin R (⇑f ⁻¹' {0}) ≤ S
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (star x * y) = star y * x

Tactic:
star_mul,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star y * star (star x) = star y * x
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (x * star y) = y * star x

Tactic:
star_mul,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (star y) * star x = y * star x
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddMonoid (R i)
inst✝ : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
x✝ : ι
⊢ star (single i r) x✝ = single i (star r) x✝

Tactic:
exact apply_single (fun _ ↦ star) (fun _ ↦ star_zero _) ..

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

Goal state before:
pp: R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)

Tactic:
star_mul,

Goal state after:
R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star x * star y⁻¹) = (op (star y))⁻¹ * op (star x)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : Mul R
inst✝¹ : Mul S
inst✝ : StarMul S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
mul : ∀ (x y : R), f (x * y) = f x * f y
x y : R
⊢ Star.star (f x * f y) = f (Star.star y * Star.star x)

Tactic:
star_mul,

Goal state after:
R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : Mul R
inst✝¹ : Mul S
inst✝ : StarMul S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
mul : ∀ (x y : R), f (x * y) = f x * f y
x y : R
⊢ Star.star (f y) * Star.star (f x) = f (Star.star y * Star.star x)
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ (↑q • 1) • x = q • 1 • x

Tactic:
← smul_assoc

Goal state after:
M : Type u_1
R : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ (↑q • 1) • x = (q • 1) • x
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝³ : DivisionRing R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ M
inst✝ : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ (↑q • 1) • x = q • 1 • x

Tactic:
← smul_assoc

Goal state after:
M : Type u_1
R : Type u_3
inst✝³ : DivisionRing R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ M
inst✝ : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ (↑q • 1) • x = (q • 1) • x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ star (x * y) = x * y

Tactic:
star_mul,

Goal state after:
case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ star y * star x = x * y
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℕ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x y : A
⊢ ⟨⅟2 • (x + y - star (x + y)), ⋯⟩ = ⟨⅟2 • (x - star x), ⋯⟩ + ⟨⅟2 • (y - star y), ⋯⟩

Tactic:
by
    ext
    simp only [sub_add, ← smul_add, sub_sub_eq_add_sub, star_add, AddSubgroup.coe_add]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑((selfAdjointPart R) x) = x

Tactic:
selfAdjointPart_apply_coe,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • (x + star x) = x
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case zero.inl.inl
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : n
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inl i) (Sum.inl j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inl i) (Sum.inl j)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case zero.inl.inr
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : n
j : m
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inl i) (Sum.inr j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inl i) (Sum.inr j)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case zero.inr.inl
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : m
j : n
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inr i) (Sum.inl j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inr i) (Sum.inl j)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case zero.inr.inr
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : m
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inr i) (Sum.inr j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inr i) (Sum.inr j)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inl val✝) = 1 (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : l
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inr val✝) = 1 (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inl val✝) = 1 (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [one_apply]

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

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inr val✝) = 1 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp [one_apply]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℤ
⊢ LinearEquiv.baseChange R A M M (f ^ n) = LinearEquiv.baseChange R A M M f ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ n h =>
    simp only [zpow_add_one, LinearEquiv.baseChange_mul, h]
  | pred n h =>
    simp only [zpow_sub_one, LinearEquiv.baseChange_mul, h, LinearEquiv.baseChange_inv]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLinearMapRight' (M * M')) x = x

Tactic:
hMM',

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLinearMapRight' 1) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLin' (M * M')) x = x

Tactic:
hMM',

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLin' 1) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
⊢ ((toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 0

Tactic:
have := Fintype.ofFinite m
  rw [toLin_apply]
  exact ⟨Fintype.linearIndependent_iff.mp v₂.linearIndependent _, fun h ↦ by simp [h]⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) (f * g) = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g

Tactic:
by
  rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₂ v₂) (M * M')) x = x

Tactic:
hMM',

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₂ v₂) 1) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : T
ik jk : m × n
⊢ (leftMulMatrix (b.smulTower c)) x ik jk = (leftMulMatrix b) ((leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1

Tactic:
by
  simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smulTower_apply,
    Basis.smulTower_repr, Finsupp.smul_apply, smul_eq_mul, map_smul, mul_smul_comm,
    coe_lmul_eq_mul, LinearMap.mul_apply']

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst✝ : ℕ
bS : Basis ι R S
bI : Basis (Fin fst✝) R ↥(restrictScalars R I)
f✝ : Fin fst✝ ↪ ι
a✝ : Fin fst✝ → R
snf✝ : ∀ (i : Fin fst✝), ↑(bI i) = a✝ i • bS (f✝ i)
val✝ : Fintype ι
⊢ Fintype.card (Fin fst✝) = Fintype.card ι

Tactic:
exact Ideal.rank_eq bS hI (bI.map ((restrictScalarsEquiv R S S I).restrictScalars R))

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
IsLocalization.eq_iff_exists M

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 * g ↑((toLocalizationMap M S).sec x).2 *
        g ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec y).2 * g ((toLocalizationMap M S).sec x).1 *
        g ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec y).2 * g ↑((toLocalizationMap M S).sec x).2 *
      g ((toLocalizationMap M S).sec (x + y)).1

Tactic:
simp_rw [← map_mul g, ← map_add g]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g
      (((toLocalizationMap M S).sec y).1 * ↑((toLocalizationMap M S).sec x).2 *
          ↑((toLocalizationMap M S).sec (x + y)).2 +
        ↑((toLocalizationMap M S).sec y).2 * ((toLocalizationMap M S).sec x).1 *
          ↑((toLocalizationMap M S).sec (x + y)).2) =
    g
      (↑((toLocalizationMap M S).sec y).2 * ↑((toLocalizationMap M S).sec x).2 *
        ((toLocalizationMap M S).sec (x + y)).1)