mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
induction n with
  | zero => exact congr_refl_refl.symm
  | succ n ih => simp_rw [pow_succ, ih, congr_mul]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
⊢ rTensor M (g ∘ₗ f) = rTensor M g ∘ₗ rTensor M f

Tactic:
by
  ext m n
  simp only [compr₂ₛₗ_apply, mk_apply, comp_apply, rTensor_tmul]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ lTensor M (f - g) = lTensor M f - lTensor M g

Tactic:
simp_rw [← coe_lTensorHom]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M) (f - g) = (lTensorHom M) f - (lTensorHom M) g
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y * z + x) y

Tactic:
rw [add_comm]
  exact h.add_mul_left_left z

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

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : x < 0
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
rw [abs_of_neg h, IsCoprime.neg_left_iff]

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

Goal state before:
pp: x y : ℤ
h : IsCoprime x y
⊢ IsCoprime (x.gcdA y) y

Tactic:
by
  use x, x.gcdB y
  rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]

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

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

Tactic:
rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
    cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ ≤ ⊤ * P

Tactic:
conv_lhs => rw [← mul_one ⊤, ← h, ← mul_assoc]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ * N * P ≤ ⊤ * P
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsNoetherianRing R
inst✝ : IsNoetherianRing S
⊢ IsNoetherianRing (R × S)

Tactic:
rw [IsNoetherianRing, isNoetherian_iff'] at *

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : WellFoundedGT (Submodule R R)
inst✝ : WellFoundedGT (Submodule S S)
⊢ WellFoundedGT (Submodule (R × S) (R × S))
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

Tactic:
rw [hq, zero_dvd_iff] at hpq

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ p / q ∣ p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
by
  have :=
    @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
      (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
  rwa [xgcdAux_val, xgcd_val] at this

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
I J : Ideal R
inst✝ : I.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ¬(I = ⊥ ∨ J = ⊥)

Tactic:
exact not_or_intro hI hJ

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

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 ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
· intro x y _ _ hx hy
      rw [smul_add, hx, hy, zero_add]

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 ∈ span R s, r • x = 0 → r • a • x = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ I ⊔ ⊤ = ⊤

Tactic:
sup_top_eq

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

Goal state before:
pp: case neg.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * g' hb

Tactic:
hg hb

Goal state after:
case neg.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ s.gcd f * g' hb = s.gcd f * g' hb
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0; · simp
  obtain rfl | hy := eq_or_ne y 0; · simp
  simp_rw [normalize, normUnit_mul hx hy]
  ac_rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
cb : α
hb : b = gcd a b * cb
⊢ a = 0 ∧ b = 0

Tactic:
rw [h, zero_mul] at ha hb

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ d₁ ^ k ∣ a * b

Tactic:
use d₂ ^ k

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ a * b = d₁ ^ k * d₂ ^ k
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x

Tactic:
obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
x✝¹ x✝ : α
⊢ DvdNotUnit x✝¹ x✝ ↔ InvImage (fun x1 x2 ↦ x1 > x2) (fun a ↦ ⟨Ideal.span {a}, ⋯⟩) x✝¹ x✝

Tactic:
exact Ideal.span_singleton_lt_span_singleton.symm

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

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = 0
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
clear hp
    rw [Finset.card_eq_zero] at hn
    subst hn
    rw [Finset.coe_empty, Set.biUnion_empty, Set.union_empty, subset_union] at h
    simpa only [exists_prop, Finset.notMem_empty, false_and, exists_false, or_false]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Subsingleton

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ ⨆ ι, Cardinal.mk ↑↑ι ≤ ⊥

Tactic:
exact ciSup_le fun s ↦ by simp [(linearIndependent_subsingleton_iff _).mp s.2]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y

Tactic:
simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]

Goal state after:
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)
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₂

Tactic:
g

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 g : ι →₀ R
⊢ (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g →
    f = g
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 = ⊤
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₂

Tactic:
g

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 g : ι →₀ R
⊢ (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g →
    f = g
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
hat : i ∉ insert b u
hp : ∀ i_1 ∈ insert i (insert b u), i_1 ≠ i → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i (insert b u)), ↑(f i_1)
has : i ∈ insert i (insert b u)
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
u : Finset ι
i : ι
hiu : i ∈ u
hbu : i ∉ u
hat : a ∉ insert i u
hp : ∀ i_1 ∈ insert a (insert i u), i_1 ≠ a → i_1 ≠ i → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert a (insert i u)), ↑(f i_1)
has : a ∈ insert a (insert i u)
hbt : i ∈ insert i u
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
j : ι
hj : j ∈ t
hat : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ j → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert j t), ↑(f i)
has : j ∈ insert j t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ j → (f i).IsPrime
hbt : j ∉ t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert b t, i ≠ j → i ≠ b → (f i).IsPrime
has : j ∉ insert b t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
j : ι
hj : j ∈ t
hbt : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ a → i ≠ j → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert j t), ↑(f i)
has : a ∉ insert j t
hbs : j ∈ insert j t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ j → i_1 ≠ b → (f i_1).IsPrime
has : j ∉ insert i t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ j → (f i_1).IsPrime
hbs : j ∉ insert i t
⊢ False

Tactic:
solve_by_elim only [Finset.mem_insert_of_mem, *]

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✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
⊢ (single i j r).submatrix ⇑f ⇑g = single (f.symm i) (g.symm j) r

Tactic:
by
  ext i' j'
  dsimp
  obtain hi | rfl := ne_or_eq (f.symm i) i'
  · rw [single_apply_of_row_ne hi, single_apply_of_row_ne]
    exact f.symm_apply_eq.not.1 hi
  obtain hj | rfl := ne_or_eq (g.symm j) j'
  · rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne]
    exact g.symm_apply_eq.not.1 hj
  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
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
rw [Classical.or_iff_not_imp_left]
  intro ha
  obtain ⟨c, i, hi, hc⟩ := exists_inv_pow I ha n
  obtain hb := congr($hc * b)
  rw [one_mul] at hb
  rw [← hb, add_mul, mul_assoc]
  exact add_mem (mul_mem_left _ _ h) (mul_mem_right _ _ hi)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
· inhabit α
      exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

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

Goal state before:
pp: F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
rw [SetLike.mem_coe, mem_range, Set.mem_range]

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

Goal state before:
pp: case zero
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : x ∈ adjoin R s
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx

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

Goal state before:
pp: case toFun
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2

Tactic:
exact AlgebraTensorModule.lift <|
      toModule S _ _ fun i₁ => flip <| toModule R _ _ fun i₂ => flip <| AlgebraTensorModule.curry <|
      DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ (linearCombination R id) (((b.constr ℕ) fun i ↦ Finsupp.single (b i) 1) m) = m

Tactic:
simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
    map_finsuppSum]

Goal state after:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ ((b.repr m).sum fun a b_1 ↦ b_1 • b a) = m
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v : N
⊢ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (r • v)))) =
    (RingHom.id S) r • mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm v)))

Tactic:
by ext i; simp [e₁, e₂.symm.map_smulₛₗ]

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

Goal state before:
pp: case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ 0 k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj),

Goal state after:
case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ 0 k' l' = 0
Module: Mathlib.Algebra.Star.Basic

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

Tactic:
star_star

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star y * 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 (star y) * star x = y * star x

Tactic:
star_star

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

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

Tactic:
star_star

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝¹ : Star R
inst✝ : InvolutiveStar S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
r : R
⊢ Star.star (Star.star (f r)) = f r

Tactic:
star_star

Goal state after:
R : Type u
S : Type v
f : R → S
inst✝¹ : Star R
inst✝ : InvolutiveStar S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
r : R
⊢ f r = f r
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint ((algebraMap R A) r)

Tactic:
simpa using! congr(algebraMap R A $(hr.star_eq))

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b'.repr ((b.prod b') (Sum.inr i)).2 = b'.repr (b' i)

Tactic:
by
    ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.snd_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inr_injective

Goal state after: