mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: m n : ℕ
⊢ IsCoprime ↑m ↑n ↔ m.Coprime n

Tactic:
Int.isCoprime_iff_gcd_eq_one,

Goal state after:
m n : ℕ
⊢ (↑m).gcd ↑n = 1 ↔ m.Coprime n
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
⊢ ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j

Tactic:
let li := List.ofFn val

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
⊢ ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i ≤ toInt val j ↔ ¬val i ≤ val j

Tactic:
simpa using toInt_lt_toInt val j i

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

Goal state before:
pp: case refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
⊢ (↑t).Pairwise (IsCoprime on s)

Tactic:
· rintro i hi j hj h
    apply IsCoprime.prod_right_iff.mp (hp i hi)
    exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h xz = x * h z
⊢ x * h z = h xz

Tactic:
hxz

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h xz = x * h z
⊢ x * h z = x * h z
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
f : R →ₗ[R] M
⊢ map f I ≤ I • ⊤

Tactic:
by
  rintro _ ⟨y, hy, rfl⟩
  rw [← mul_one y, ← smul_eq_mul, f.map_smul]
  exact smul_mem_smul hy mem_top

Goal state after:
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
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ x ∈ M'

Tactic:
suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
    rw [← LinearMap.toSpanSingleton_apply_one R M x]
    exact this (LinearMap.mem_range_self _ 1)

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ (LinearMap.toSpanSingleton R M x).range ≤ M'
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a : K
ha : a ≠ 0
b : K
⊢ EuclideanDomain.gcd a b = a

Tactic:
rw [Field.gcd_eq, if_neg ha]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b

Tactic:
rw [gcd_zero_left]
      exact ⟨dvd_zero _, dvd_rfl⟩

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ (map f I).IsMaximal ↔ I.IsMaximal

Tactic:
by
  simpa only [isMaximal_def] using! (relIsoOfBijective _ hf).symm.isCoatom_iff _

Goal state after:
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 *
  rw [Submodule.span_smul_span, I.span_eq]

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✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
r : R
h : f r ∈ map f I
s : R
hsi : s ∈ ↑I
hfsr : f s = f r
⊢ f r - f r = 0

Tactic:
sub_self

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
r : R
h : f r ∈ map f I
s : R
hsi : s ∈ ↑I
hfsr : f s = f r
⊢ 0 = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (m : ↥N), r • m = 0) ↔ ∀ n ∈ N, r • n = 0

Tactic:
Subtype.forall,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), r • ⟨a, b⟩ = 0) ↔ ∀ n ∈ N, r • n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this : ∀ I ∈ A, f x' ∈ map f I
⊢ f x' - f x' = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this : ∀ I ∈ A, f x' ∈ map f I
⊢ 0 = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = replicate s.card (s.gcd * 1) ∧ (replicate s.card 1).gcd = 1

Tactic:
eq_replicate,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = s.gcd * 1) ∧ (replicate s.card 1).gcd = 1
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.gcd f = GCDMonoid.gcd 0 (s₂.gcd f)

Tactic:
gcd_zero_left,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.gcd f = normalize (s₂.gcd f)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ Codisjoint I J ↔ I + J = 1

Tactic:
codisjoint_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ ↔ I + J = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
⊢ Codisjoint (span {x}) (span {y}) ↔ IsCoprime x y

Tactic:
codisjoint_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y
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)
k : ℕ
h : b * a = c ^ 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'
⊢ Associated (d₁ ^ k) a

Tactic:
(gcd_comm' a b).isUnit_iff

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h : b * a = c ^ 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'
⊢ Associated (d₁ ^ k) a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ r ^ (n + k) ∈ m

Tactic:
rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c * x),
                      mul_assoc c x (d * y), mul_left_comm x, ← mul_assoc]
                  refine
                    m.add_mem (m.mul_mem_right _ hpm)
                    (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
⊢ a = 0 ∨ b = 0 → lcm a b = 0

Tactic:
rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right]

Goal state after:
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:
exact
    ⟨strongNormalizedGCDMonoidOfExistsGCD fun _ _ ↦ ⟨_, fun _ ↦ (dvd_gcd_iff ..).symm⟩⟩

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

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ : Type v
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
ι : Type w
ι' : Type w'
inst✝⁶ : StrongRankCondition R✝
R : Type ?u.18
M : Type ?u.22
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Finite ι
b : Basis ι R M
P : Submodule R M → Sort u_2
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
N : Submodule R M
this : Fintype ι := Fintype.ofFinite ι
m✝ : ℕ
hs : Fin m✝ → ↥N
hli : LinearIndependent R (Subtype.val ∘ hs)
⊢ m✝ ≤ Fintype.card ι

Tactic:
by
    simpa using b.card_le_card_of_linearIndependent hli

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✝ : StrongRankCondition R
ι : Type w
b : Finset ι
h : Basis (↥b) R M
⊢ finrank R M = b.card

Tactic:
finrank_eq_card_basis h,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Finset ι
h : Basis (↥b) R M
⊢ Fintype.card ↥b = b.card
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
by
  refine ⟨?_, ?_, ?_, ?_⟩ <;>
  · rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
⊢ 1 * M = M

Tactic:
ext
  rw [← diagonal_one, diagonal_mul, one_mul]

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

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

Tactic:
rw [mulVec_neg, neg_mulVec, neg_neg]

Goal state after:
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 : (M ^ k).row i = 0
h' : k ≤ l
⊢ (M ^ l).row i = 0

Tactic:
replace h' : l = k + (l - k) := by lia
  rw [← single_one_vecMul] at h ⊢
  rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
e : m ≃ n
M : Matrix m n α
⊢ M.submatrix id ⇑e * Mᵀ.submatrix (⇑e) id = M * Mᵀ

Tactic:
submatrix_mul_equiv,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
e : m ≃ n
M : Matrix m n α
⊢ (M * Mᵀ).submatrix id id = M * Mᵀ
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ B.submatrix ⇑(Equiv.refl n) ⇑e.symm * A.submatrix ⇑e.symm ⇑(Equiv.refl n) = 1 ↔ B * A = 1

Tactic:
submatrix_mul_equiv,

Goal state after:
m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (B * A).submatrix ⇑(Equiv.refl n) ⇑(Equiv.refl n) = 1 ↔ B * A = 1
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 ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a = s.sup' hs fun i ↦ f i + a

Tactic:
by
  apply le_antisymm
  · 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)
  · exact Finset.sup'_le _ _ fun i hi ↦ by grw [← Finset.le_sup' _ hi]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
⊢ (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y

Tactic:
by
  ext
  simp only [vecMul, sum_dotProduct, Finset.sum_apply]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J

Tactic:
rintro ⟨y, ⟨hy, ⟨z, ⟨hz, rfl⟩⟩⟩⟩; exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

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

Goal state before:
pp: ι₁ ι₂ : Type v
inst✝² : DecidableEq ι₂
f : ι₁ → ι₂
β : ι₁ → Type w
inst✝¹ : (i : ι₁) → AddCommMonoid (β i)
inst✝ : DecidableEq ι₁
i : ι₁
x : β i
h : (y : ι₂) × { x // f x = y } ≃ ι₁ := Equiv.sigmaFiberEquiv f
k : (j : ι₂) × { i₁ // f i₁ = j } := ⟨f i, ⟨i, ⋯⟩⟩
⊢ (sigmaFiberAddEquiv f) ((of β (h k)) x) = sigmaCurry ((of (fun k ↦ β ↑k.snd) k) x)

Tactic:
sigmaFiberAddEquiv_apply

Goal state after:
ι₁ ι₂ : Type v
inst✝² : DecidableEq ι₂
f : ι₁ → ι₂
β : ι₁ → Type w
inst✝¹ : (i : ι₁) → AddCommMonoid (β i)
inst✝ : DecidableEq ι₁
i : ι₁
x : β i
h : (y : ι₂) × { x // f x = y } ≃ ι₁ := Equiv.sigmaFiberEquiv f
k : (j : ι₂) × { i₁ // f i₁ = j } := ⟨f i, ⟨i, ⋯⟩⟩
⊢ sigmaCurry ((equivCongrLeft (Equiv.sigmaFiberEquiv f).symm) ((of β (h k)) x)) =
    sigmaCurry ((of (fun k ↦ β ↑k.snd) k) x)
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0

Tactic:
change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _
  simp [h.ofBijective_coeLinearMap_of_mem_ne hij hx]

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

Goal state before:
pp: case a.smul
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
x✝ : A
r : R
x : A
hx✝ : x ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x ∈ span R ↑(Subsemigroup.closure s)

Tactic:
| smul r x _ hpx =>

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

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

Tactic:
apply op_injective

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

Tactic:
isSelfAdjoint_iff,

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 (x * y) = x * y
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarMul R
x : R
inst✝ : Invertible x
⊢ IsSelfAdjoint ⅟x ↔ IsSelfAdjoint x

Tactic:
isSelfAdjoint_iff,

Goal state after:
R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarMul R
x : R
inst✝ : Invertible x
⊢ star ⅟x = ⅟x ↔ IsSelfAdjoint x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarMul R
x : R
inst✝ : Invertible x
⊢ star ⅟x = ⅟x ↔ IsSelfAdjoint x

Tactic:
isSelfAdjoint_iff,

Goal state after:
R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarMul R
x : R
inst✝ : Invertible x
⊢ star ⅟x = ⅟x ↔ star x = x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: A : Type u_2
a : A
inst✝¹ : Semiring A
inst✝ : StarRing A
ha : IsSelfAdjoint a
⊢ IsSelfAdjoint a⁻¹ʳ

Tactic:
isSelfAdjoint_iff,

Goal state after:
A : Type u_2
a : A
inst✝¹ : Semiring A
inst✝ : StarRing A
ha : IsSelfAdjoint a
⊢ star a⁻¹ʳ = a⁻¹ʳ
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : Star R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : Monoid R
inst✝¹ : DistribMulAction R A
inst✝ : StarModule R A
r : R
x : A
h : x ∈ skewAdjoint A
⊢ star r • star x = -(r • x)

Tactic:
star_trivial,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁶ : Star R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : Monoid R
inst✝¹ : DistribMulAction R A
inst✝ : StarModule R A
r : R
x : A
h : x ∈ skewAdjoint A
⊢ r • star x = -(r • x)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : IsStarNormal a
hb : IsStarNormal b
⊢ IsStarNormal (a + b)

Tactic:
rw [isStarNormal_iff] at ha hb ⊢

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star (a + b)) (a + b)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : IsStarNormal a
hb : IsStarNormal b
⊢ IsStarNormal (a + b)

Tactic:
rw [isStarNormal_iff] at ha hb ⊢
  have := _root_.star_star b ▸ hab.star_star
  simp only [star_add, commute_iff_eq, mul_add, add_mul]
  rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v).map star = diagonal (star v)

Tactic:
diagonal_map (star_zero _)

Goal state after:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal fun m ↦ star (v m)) = diagonal (star v)
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
⊢ star ⅟2 • star (x + star x) = ⅟2 • (x + star x)

Tactic:
star_trivial,

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
⊢ ⅟2 • star (x + star x) = ⅟2 • (x + star x)
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 : ι
j : ι'
⊢ (single (Sum.inl i) 1) (Sum.inr j) = 0

Tactic:
apply Finsupp.single_eq_of_ne Sum.inr_ne_inl

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
u : M
hu : u ∈ range v
⊢ u ∈ ↑p

Tactic:
obtain ⟨i, rfl⟩ := hu

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
⊢ v i ∈ ↑p
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᵀ = blockDiagonal' fun k ↦ (M k)ᵀ

Tactic:
by
  ext ⟨ii, ix⟩ ⟨ji, jx⟩
  simp only [transpose_apply, blockDiagonal'_apply]
  split_ifs <;> grind

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

Goal state before:
pp: R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q).symm (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q)) = (a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)

Tactic:
apply ((distribBaseChange R A N Q).eq_symm_apply.mpr ?_).symm

Goal state after:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q) ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)) = a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_2
α : Type u_1
x y : α
h : x ≠ y
a b : Fin (Nat.succ 0).succ
h' : ![x, y] a = ![x, y] b
⊢ a = b

Tactic:
fin_cases a

Goal state after:
case refine_2.«0»
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩) = ![x, y] b
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = b

case refine_2.«1»
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩) = ![x, y] b
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = b