mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
· refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
      rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : Group α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S

Tactic:
rw [mem_nonunits_iff, isUnit_iff]

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

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

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

Tactic:
· simp

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

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

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
⊢ normalize (x * y) = normalize x * normalize y
Module: Mathlib.Algebra.GCDMonoid.Basic

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

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

Tactic:
· simp

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalize (x * y) = normalize x * normalize y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) → IsCoprime x y

pp: case mpr
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ a b, y ∣ b ∧ a * x + b = 1

Tactic:
· rintro ⟨a, _, ⟨b, rfl⟩, e⟩; exact ⟨a, b, mul_comm b y ▸ e⟩

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ a b, y ∣ b ∧ a * x + b = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp1 : (↑s).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ ∀ j ∈ s, IsCoprime (J a) (J j)

Tactic:
by grind

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : IsBezout R
x y : R
⊢ IsPrincipal (Ideal.span {x, y})

Tactic:
exact isPrincipal_of_FG (Ideal.span {x, y}) ⟨{x, y}, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
⊢ 1 ∈ T

Tactic:
obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
        have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
        rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
        exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ if h : a = 0 then ∅ else Classical.choose ⋯, Irreducible b) ∧
    Associated (if h : a = 0 then ∅ else Classical.choose ⋯).prod a

Tactic:
rw [dif_neg h]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ Classical.choose ⋯, Irreducible b) ∧ Associated (Classical.choose ⋯).prod a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ S.IsPrincipal

Tactic:
by
  rw [← Submodule.map_comap_eq_of_surjective hf S]
  exact hI.map f

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
h : Function.Injective fun x ↦ x ⬝ᵥ a
b : m → α
hb : b ≠ 0
hba : b ⬝ᵥ a = 0
⊢ False

Tactic:
simpa [hba, hb] using @h b 0

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

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ (∑ i_1, if i = i ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i

pp: case inr
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h : i ≠ i'
⊢ (∑ i_1, if i = i' ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i'

Tactic:
· simp

Goal state after:
case inr
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h : i ≠ i'
⊢ (∑ i_1, if i = i' ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
by
  rcases Set.Finite.exists_finset hs with ⟨t, ht⟩
  have heq : ⋃ i ∈ s, f i = ⋃ i ∈ t, (f i : Set R) := by
    ext
    simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)
  have hmem_union : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ((I : Set R) ⊆ ⋃ i ∈ (t : Set ι), f i) :=
    (congrArg _ heq).to_iff
  rw [hmem_union, Ideal.subset_union_prime a b (fun i hin ↦ hp i ((ht i).mp hin))]
  exact exists_congr (fun i ↦ and_congr_left fun _ ↦ ht i)

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 l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

Tactic:
by_cases h₁ : i = a <;> by_cases h₂ : k = b

Goal state after:
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 : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

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 : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

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 : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

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 : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
h : (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) B
i : m
j : n
⊢ A i j = B i j

Tactic:
classical
  simpa using congrFun₂ h (Pi.single i 1) j

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

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_3
β : Type u_2
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⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
i : ι
y : α
hi : y ∈ S i
h : f i ⟨y, hi⟩ ∈ t
hxy : inclusion ⋯ ⟨y, hi⟩ = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t

Tactic:
obtain rfl : y = x := congr_arg Subtype.val hxy

Goal state after:
case mpr
α : Type u_1
ι : Sort u_3
β : Type u_2
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⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : f i ⟨↑x, hi⟩ ∈ t
hxy : inclusion ⋯ ⟨↑x, hi⟩ = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ (diagonal fun m ↦ f ((algebraMap R (n → α)) r m)) = diagonal ((algebraMap R (n → β)) r)

Tactic:
simp [hf₂]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
⊢ I.ringCon ⊔ J.ringCon ≤ s.ringCon

Tactic:
refine sup_le (fun x y h => ?_) (fun x y h => ?_)

Goal state after:
case mp.refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : I.ringCon x y
⊢ s.ringCon x y

case mp.refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : J.ringCon x y
⊢ s.ringCon x y
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ x y : ⨁ (i : ι), M
ihx : (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) x) = x
ihy : (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) y) = y
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) (x + y)) = x + y

Tactic:
by grind

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
h : ι ≃ κ
k : κ
x : M (h.symm k)
⊢ (lequivCongrLeft R h).symm ((lof R κ (fun k ↦ M (h.symm k)) k) x) = (lof R ι M (h.symm k)) x

Tactic:
LinearEquiv.symm_apply_eq

Goal state after:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
h : ι ≃ κ
k : κ
x : M (h.symm k)
⊢ (lof R κ (fun k ↦ M (h.symm k)) k) x = (lequivCongrLeft R h) ((lof R ι M (h.symm 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
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (coeLinearMap A) x = DFinsupp.sum x fun i x ↦ ↑x

Tactic:
simp only [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk,
    AddHom.coe_mk]
  rw [DFinsupp.sumAddHom_apply]
  simp only [LinearMap.toAddMonoidHom_coe, Submodule.coe_subtype]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
by
              let ⟨k, hik, hjk⟩ := dir i j
              rw [hf i k hik, hf j k hjk]
              rfl

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ Star.star (r • f x) = f (Star.star r • Star.star x)

Tactic:
star_smul,

Goal state after:
R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ Star.star r • Star.star (f x) = f (Star.star r • Star.star x)
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 • x) = -(r • x)

Tactic:
star_smul,

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
⊢ star r • star x = -(r • x)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : MulOneClass R
inst✝ : StarMul R
⊢ Commute (star 1) 1

Tactic:
by simp only [Commute.refl, star_one]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Star B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Star C
inst✝¹ : NonUnitalNonAssocSemiring D
inst✝ : Star D
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Star B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Star C
inst✝¹ : NonUnitalNonAssocSemiring D
inst✝ : Star D
f : A → B
map_mul'✝¹ : ∀ (x y : A), f (x * y) = f x * f y
map_zero'✝¹ : { toFun := f, map_mul' := map_mul'✝¹ }.toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_mul' := map_mul'✝¹ }.toFun (x + y) =
      { toFun := f, map_mul' := map_mul'✝¹ }.toFun x + { toFun := f, map_mul' := map_mul'✝¹ }.toFun y
map_star'✝¹ :
  ∀ (a : A),
    { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (star a) =
      star ({ toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun a)
g : A → B
map_mul'✝ : ∀ (x y : A), g (x * y) = g x * g y
map_zero'✝ : { toFun := g, map_mul' := map_mul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    { toFun := g, map_mul' := map_mul'✝ }.toFun (x + y) =
      { toFun := g, map_mul' := map_mul'✝ }.toFun x + { toFun := g, map_mul' := map_mul'✝ }.toFun y
map_star'✝ :
  ∀ (a : A),
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (star a) =
      star ({ toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun a)
h :
  (fun f ↦ f.toFun)
      { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        map_star' := map_star'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }
⊢ { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_star' := map_star'✝¹ } =
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }
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 • (x + star x)) = ⅟2 • (x + star x)

Tactic:
star_smul,

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
⊢ star ⅟2 • star (x + star x) = ⅟2 • (x + star x)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j

Tactic:
rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
      exact Prod.fst_eq_iff.mpr

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

Goal state before:
pp: case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then of (fun i_1 j ↦ if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j ↦ if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨i, k'⟩

pp: case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then of (fun i_1 j ↦ if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j ↦ if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩

Tactic:
· simp

Goal state after:
case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then of (fun i_1 j ↦ if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j ↦ if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
⊢ N = ⊥

Tactic:
rw [Submodule.eq_bot_iff]
  intro x hx
  refine b.ext_elem fun i ↦ ?_
  rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ
  rw [map_zero, Finsupp.zero_apply]
  exact
    (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _
      ⟨x, hx, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ ⨆ i, span R ((fun x ↦ M.vecMulLinear ((LinearMap.single R (fun i ↦ R) i) x)) '' {1}) = span R (Set.range M.row)

Tactic:
image_singleton,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ ⨆ i, R ∙ M.vecMulLinear ((LinearMap.single R (fun i ↦ R) i) 1) = span R (Set.range M.row)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : K
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Goal state after: