mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ 1 * a ↔ x ∈ a

Tactic:
simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1, ∃ z ∈ a, a_1 • z = x) ↔ x ∈ a
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
⊢ ∀ (a b : α), (decide (a ≤ b) || decide (b ≤ a)) = true

Tactic:
by simpa using le_total

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

Goal state before:
pp: case cons.mp.refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
· have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_sdiff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

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

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
⊢ ∀ (s_1 : Finset I),
    a ∉ s_1 →
      ((↑s_1).Pairwise (IsRelPrime on s) → (∀ i ∈ s_1, s i ∣ z) → ∏ x ∈ s_1, s x ∣ z) →
        (↑(insert a s_1)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a s_1, s i ∣ z) → ∏ x ∈ insert a s_1, s x ∣ z

Tactic:
r

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
⊢ a ∉ r →
    ((↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z) →
      (↑(insert a r)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a r, s i ∣ z) → ∏ x ∈ insert a r, s x ∣ z
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ ∏ i ∈ insert a✝ s✝, span R (M i) = span R (∏ i ∈ insert a✝ s✝, M i)

Tactic:
rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]

Goal state after:
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
M₁ M₂ : Submodule R N
inst✝¹ : IsNoetherian R ↥M₁
inst✝ : IsNoetherian R ↥M₂
⊢ IsNoetherian R ↥(M₁ ⊔ M₂)

Tactic:
by
  have := isNoetherian_range (M₁.subtype.coprod M₂.subtype)
  rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this

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

Goal state before:
pp: case h.zero
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ 0
⊢ f 0 = ⊥

pp: case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊥

Tactic:
· cases p

Goal state after:
case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊥
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hT : T.FG
hST : S ≤ T
⊢ S.FG

Tactic:
← Module.Finite.iff_fg

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hT : Module.Finite R ↥T
hST : S ≤ T
⊢ S.FG
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (↑f) (comap (↑f.symm) I) = I

Tactic:
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z

Tactic:
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y / gcd x y ∣ z
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ker f = ⊥

Tactic:
SetLike.ext'_iff,

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0

Tactic:
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ gcd x y * (x * y / gcd x y) = x * y
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * c * (a * b) / (a * c) = a * b

Tactic:
mul_div_cancel_left₀ _ (mul_ne_zero ha hc)

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b = a * b
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Tactic:
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
  simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) ↔ Codisjoint I J

Tactic:
codisjoint_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) ↔ I ⊔ J = ⊤
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
convert ← (assoc 1).choose_spec

Goal state after:
case e'_2
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ 1 * ↑(Exists.choose ⋯) = ↑(if 1 = 0 then 1 else Exists.choose ⋯)

case e'_3
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ out (Associates.mk 1) = ↑1
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
codisjoint_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
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:
| cons a s has ih =>

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ (s.inf f).radical = (f i).radical

Tactic:
by
  rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]
  exact Finset.inf'_eq_of_forall _ _ hs

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
S : Ideal K
⊢ IsPrincipal S

Tactic:
rcases Ideal.eq_bot_or_top S with (rfl | rfl)

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊥

case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊤
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a ∈ R ∙ 0

Tactic:
rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]

Goal state after:
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a = 0
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

Tactic:
simp [Set.eq_empty_iff_forall_notMem, isPrincipalIdealRing_iff]

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

Goal state before:
pp: case neg
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
· rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]

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
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ Nontrivial M

Tactic:
rw [← not_subsingleton_iff_nontrivial]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ ¬Subsingleton M
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔ ¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀

Tactic:
push Not
    refine ⟨fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩, fun ⟨n, le⟩ ↦
      ⟨n, le_rank_iff_exists_linearMap.mp (natCast_le_aleph0.trans le)⟩⟩
    have ⟨g, hg⟩ := f.exists_finsupp_nat_of_fin_fun_injective inj
    convert! (Finsupp.basisSingleOne.linearIndependent.map_injOn _ hg.injOn).cardinal_lift_le_rank
    simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DistribSMul R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
b : R
v : n → α
x✝ : m
⊢ (M *ᵥ b • v) x✝ = (b • M *ᵥ v) x✝

Tactic:
exact dotProduct_smul _ _ _

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
b : n
hbj : b ≠ j
M : Matrix l m α
⊢ (M * single i j c) a b = 0

Tactic:
by simp [mul_apply, hbj.symm]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype m
inst✝¹ : DistribSMul R α
inst✝ : SMulCommClass R α α
v : m → α
b : R
M : Matrix m n α
x✝ : n
⊢ (v ᵥ* (b • M)) x✝ = (b • v ᵥ* M) x✝

Tactic:
exact dotProduct_smul _ _ _

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
rw [smulTower', repr_reindex_apply, smulTower_repr]; rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix n m R
v : n → R
i : m
⊢ f ((v ᵥ* M) i) = (⇑f ∘ v ᵥ* M.map ⇑f) i

Tactic:
simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)

Tactic:
have : x = Set.inclusion (Set.subset_iUnion S i) ⟨x, hi⟩ := by
    cases x
    rfl

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion ⋯ ⟨↑x, hi⟩
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
f : α →₀ ℕ
i : α
⊢ i ∈ toMultiset f ↔ i ∈ f.support

Tactic:
← Multiset.count_ne_zero,

Goal state after:
α : Type u_1
f : α →₀ ℕ
i : α
⊢ Multiset.count i (toMultiset f) ≠ 0 ↔ i ∈ f.support
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
⊢ φ.equalizer ψ = ⊤ ↔ φ = ψ

Tactic:
by
  simp [SetLike.ext_iff, DFunLike.ext_iff]

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
⊢ 0 ∈ {a | ϕ a = ψ a}

Tactic:
rw [Set.mem_ofPred_eq, map_zero, map_zero]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑((x • s) • t) = ↑(x • s • t)

Tactic:
rw [← one_smul R s, ← smul_assoc, one_smul, ← one_smul R (s • t), ← smul_assoc,
      Algebra.smul_def, Algebra.smul_def]
    apply mul_assoc

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

Goal state before:
pp: case a.cons.nil
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
HL : ∀ y ∈ [], y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = [].prod

Tactic:
exact ⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ (linearCombination R id ∘ₗ g) (i x) = x

Tactic:
hg,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ s (i x) = x
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ finsuppTensorFinsuppRid R R ι κ =
    (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R R))

Tactic:
finsuppTensorFinsuppRid,

Goal state after:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R)) =
    (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R R))
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype I
inst✝ : Fintype J
x✝¹ x✝ : Matrix I I (Matrix J J R)
⊢ (compAddEquiv I I J J R).toFun (x✝¹ * x✝) = (compAddEquiv I I J J R).toFun x✝¹ * (compAddEquiv I I J J R).toFun x✝

Tactic:
by ext; exact sum_apply .. |>.trans <| .symm <| Fintype.sum_prod_type ..

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : AddMonoid R
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
add : ∀ (x y : R), f (x + y) = f x + f y
x y : R
⊢ Star.star (f (x + y)) = f (Star.star x + Star.star y)

Tactic:
add,

Goal state after:
R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : AddMonoid R
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
add : ∀ (x y : R), f (x + y) = f x + f y
x y : R
⊢ Star.star (f x + f y) = f (Star.star x + Star.star y)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : AddMonoid R
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
add : ∀ (x y : R), f (x + y) = f x + f y
x y : R
⊢ Star.star (f x) + Star.star (f y) = f (Star.star x + Star.star y)

Tactic:
add,

Goal state after:
R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : AddMonoid R
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
add : ∀ (x y : R), f (x + y) = f x + f y
x y : R
⊢ Star.star (f x) + Star.star (f y) = f (Star.star x) + f (Star.star y)
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = map N.subtype ⊤

Tactic:
Submodule.map_subtype_top

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = N
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = map N.subtype ⊤

Tactic:
Submodule.map_subtype_top

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = N
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
⊢ fromBlocks 1 0 0 1 = 1

Tactic:
by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [one_apply]

Goal state after: