mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : α✝ ≃ β✝
h : ∀ {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:
_

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.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
⊢ ∀ [Fintype α✝],
    (∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : Option α✝ → Submodule R N} [∀ (i : Option α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
_

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
inst✝ : Fintype α✝
⊢ (∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
    ∀ {M : Option α✝ → Submodule R N} [∀ (i : Option α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
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
inst✝ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
⊢ ∀ {M : Option α✝ → Submodule R N} [∀ (i : Option α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
_

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
inst✝ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
⊢ ∀ [∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)], IsNoetherian R ↥(⨆ i, M✝ i)
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
inst✝ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
⊢ ∀ [∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)], IsNoetherian R ↥(⨆ i, M✝ i)

Tactic:
_

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
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
s : Set M
x : M
⊢ x ∈ I • span R s ↔ x ∈ span R (↑I • s)

Tactic:
rw [← I.span_eq] at *

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : (Ideal.span ↑I).IsTwoSided
s : Set M
x : M
⊢ x ∈ Ideal.span ↑I • span R s ↔ x ∈ span R (↑(Ideal.span ↑I) • s)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
n : ℕ
ih : span {s} ^ n = span {s ^ n}
ne : n ≠ 0
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}

Tactic:
simp only [Submodule.pow_succ' _ ne, pow_succ', ih, span_singleton_mul_span_singleton]

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

Goal state before:
pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
⊢ x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

Tactic:
_

Goal state after:
case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx✝ : x ∈ span R s
⊢ y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) =
    GCDMonoid.lcm a (GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)))

Tactic:
← lcm_assoc,

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) =
    GCDMonoid.lcm (GCDMonoid.lcm a a) (fold GCDMonoid.lcm 1 (s.erase a))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx✝ : x ∈ span R s
⊢ y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

Tactic:
_

Goal state after:
case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx✝ : x ∈ span R s
hy✝ : y ∈ span R s
⊢ r • x = 0 → r • y = 0 → r • (x + y) = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
a : R
x : M
⊢ x ∈ span R s → r • x = 0 → r • a • x = 0

Tactic:
_

Goal state after:
case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
a : R
x : M
hx✝ : x ∈ span R s
⊢ r • x = 0 → r • a • x = 0
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 ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0

Tactic:
_

Goal state after:
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
⊢ {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
_

Goal state after:
case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
⊢ (t.gcd fun x ↦ a * f x) = normalize a * t.gcd f →
    ((insert b t).gcd fun x ↦ a * f x) = normalize a * (insert b t).gcd f
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
⊢ b ∉ s →
    ((∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)) →
      (∀ x ∈ insert b s, a ∣ f x - g x) → GCDMonoid.gcd a ((insert b s).gcd f) = GCDMonoid.gcd a ((insert b s).gcd g)

Tactic:
_

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
⊢ ((∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)) →
    (∀ x ∈ insert b s, a ∣ f x - g x) → GCDMonoid.gcd a ((insert b s).gcd f) = GCDMonoid.gcd a ((insert b s).gcd g)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd a ((insert b s).gcd f) = GCDMonoid.gcd a ((insert b s).gcd g)

Tactic:
rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (g b))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ I * J ≤ P ↔ J ≤ P ∨ I ≤ P

Tactic:
Ideal.mul_le

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
r : R
⊢ Associated (generator (Ideal.span {r})) r

Tactic:
rw [← Ideal.span_singleton_eq_span_singleton]
  exact Ideal.span_singleton_generator _

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
H : c.Nonempty
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

Tactic:
obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
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 u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
this : Finite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
let := Fintype.ofFinite ι

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)
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 = of (Pi.single i (Pi.single j a))

Tactic:
by
  ext a b
  unfold single
  by_cases hi : i = a <;> by_cases hj : j = b <;> simp [*]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
obtain ⟨y, hy⟩ : ∃ y : R, y * x + i ^ n = 1 := by
    induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y✝ i : R
hmem : i ∈ I
hi : y✝ * x + i = 1
y : R
hy : y * x + i ^ n = 1
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i : ι
⊢ i ∈ a.support → ↑(if h : a i ∈ I then ⟨a i, h⟩ else 0) • v i = a i • v i

Tactic:
_

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i : ι
a✝ : i ∈ a.support
⊢ ↑(if h : a i ∈ I then ⟨a i, h⟩ else 0) • v i = a i • v i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
u v : m → α
w : n → α
i : n
⊢ (u ᵥ* vecMulVec v w) i = ((u ⬝ᵥ v) • w) i

Tactic:
simp [vecMul, dotProduct, vecMulVec, Finset.sum_mul, mul_assoc]

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✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Nonempty n
A : Matrix l m α
⊢ (Function.Injective fun B ↦ A * B) ↔ Function.Injective A.mulVec

Tactic:
refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_col fun j => ha congr(($hBC).col j)⟩

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Nonempty n
A : Matrix l m α
ha : Function.Injective fun B ↦ A * B
v w : m → α
hvw : A *ᵥ v = A *ᵥ w
⊢ v = w
Module: Mathlib.Data.Matrix.Basis

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

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

Tactic:
· simp [h₁, h, Finset.sum_eq_zero]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
⊢ Finite (ChooseBasisIndex R M)

pp: case inr
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
⊢ Finite (ChooseBasisIndex R M)

Tactic:
· have := Module.subsingleton R M
    rw [ChooseBasisIndex]
    infer_instance

Goal state after:
case inr
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
⊢ Finite (ChooseBasisIndex R M)
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
← vecMul_vecMul,

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
⊢ (A *ᵥ x) ᵥ* B = x ᵥ* Aᵀ ᵥ* B
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
⊢ Pi.single i 1 ᵥ* (M ^ k * M ^ (l - k)) = 0

Tactic:
← vecMul_vecMul,

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
⊢ Pi.single i 1 ᵥ* M ^ k ᵥ* M ^ (l - k) = 0
Module: Mathlib.Algebra.Order.Group.Finset

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

Tactic:
apply add_le_of_le_tsub_right_of_le
    · exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self
    · exact Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)

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

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

Tactic:
simp_rw [add_comm a, Finset.sup'_add']

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
⊢ a ∉ f.support →
    n ≠ 0 →
      Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
        Multiset.map g (toMultiset (single a n + f)) = toMultiset (mapDomain g (single a n + f))

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝ : a ∉ f.support
⊢ n ≠ 0 →
    Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
      Multiset.map g (toMultiset (single a n + f)) = toMultiset (mapDomain g (single a n + f))
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝ : a ∉ f.support
⊢ n ≠ 0 →
    Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
      Multiset.map g (toMultiset (single a n + f)) = toMultiset (mapDomain g (single a n + f))

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
⊢ Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
    Multiset.map g (toMultiset (single a n + f)) = toMultiset (mapDomain g (single a n + f))
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
⊢ a ∉ f.support →
    n ≠ 0 →
      ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
        (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n ↦ a ^ n

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝ : a ∉ f.support
⊢ n ≠ 0 →
    ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
      (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n ↦ a ^ n
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝ : a ∉ f.support
⊢ n ≠ 0 →
    ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
      (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n ↦ a ^ n

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
⊢ ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
    (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n ↦ a ^ n
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: case pos
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : i = j
⊢ 0 ≤ 1 i j

Tactic:
subst hi
    simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
⊢ ∀ {x y : M}, c x y → d x y

Tactic:
_

Goal state after:
case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
x✝ : M
⊢ ∀ {y : M}, c x✝ y → d x✝ y
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
x✝ : M
⊢ ∀ {y : M}, c x✝ y → d x✝ y

Tactic:
_

Goal state after:
case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
x✝ y✝ : M
⊢ c x✝ y✝ → d x✝ y✝
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Mul M
c d : Con M
h : ∀ {x y : M}, c x y → d x y
⊢ ∀ {x y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y

Tactic:
_

Goal state after:
case mpr
M : Type u_1
inst✝ : Mul M
c d : Con M
h : ∀ {x y : M}, c x y → d x y
x✝ : Mᵐᵒᵖ
⊢ ∀ {y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x✝ y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x✝ y
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Mul M
c d : Con M
h : ∀ {x y : M}, c x y → d x y
x✝ : Mᵐᵒᵖ
⊢ ∀ {y : Mᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x✝ y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x✝ y

Tactic:
_

Goal state after:
case mpr
M : Type u_1
inst✝ : Mul M
c d : Con M
h : ∀ {x y : M}, c x y → d x y
x✝ y✝ : Mᵐᵒᵖ
⊢ ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x✝ y✝ →
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x✝ y✝