mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ f ((r • s) • x✝) = f (r • s • x✝)

Tactic:
f.map_smul_of_tower r,

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ f ((r • s) • x✝) = r • f (s • x✝)
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case fst
M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulZeroClass R M
inst✝ : SMulZeroClass R N
x✝ : R
⊢ (x✝ • 0).1 = 0.1

Tactic:
exact smul_zero _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case snd
M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulZeroClass R M
inst✝ : SMulZeroClass R N
x✝ : R
⊢ (x✝ • 0).2 = 0.2

Tactic:
exact smul_zero _

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ (l - k + k)) m = 0

Tactic:
pow_add,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ (l - k) * f ^ k) m = 0
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ (f ^ (c + n)) x = 0

Tactic:
pow_add,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ (f ^ c * f ^ n) x = 0
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • ((algebraMap R A) x✝¹ * (algebraMap R A) x✝) = x✝² • (algebraMap R A) x✝¹ * x✝² • (algebraMap R A) x✝

Tactic:
MulSemiringAction.smul_mul

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • (algebraMap R A) x✝¹ * x✝² • (algebraMap R A) x✝ = x✝² • (algebraMap R A) x✝¹ * x✝² • (algebraMap R A) x✝
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.mem.mul
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y

Tactic:
obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
y : ↥s'
⊢ ((↑e.symm).restrict s s' ⋯) ((↑↑((↑e).restrict s' s ⋯)).toFun y) = y

Tactic:
by simp [← Subtype.val_inj]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
x : ↥s
⊢ (↑↑((↑e).restrict s' s ⋯)).toFun (((↑e.symm).restrict s s' ⋯) x) = x

Tactic:
by simp [← Subtype.val_inj]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M),
      Associates.mk a ∣ Associates.mk a_1 * Associates.mk a_2 →
        ∃ x x_1,
          Associates.mk x ∣ Associates.mk a_1 ∧
            Associates.mk x_1 ∣ Associates.mk a_2 ∧ Associates.mk a = Associates.mk x * Associates.mk x_1) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
mk_mul_mk,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M),
      Associates.mk a ∣ Associates.mk (a_1 * a_2) →
        ∃ x x_1,
          Associates.mk x ∣ Associates.mk a_1 ∧
            Associates.mk x_1 ∣ Associates.mk a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk 0 * Associates.mk a = Associates.mk 0

Tactic:
mk_mul_mk,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk (0 * a) = Associates.mk 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk a * Associates.mk 0 = Associates.mk 0

Tactic:
mk_mul_mk,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk (a * 0) = Associates.mk 0
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ (-f).range = f.range

Tactic:
by
  change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _
  rw [range_comp, Submodule.map_neg, Submodule.map_id]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
p' : Submodule R ↥p
⊢ map p.subtype p' ≤ p

Tactic:
by
  simpa using (map_le_range : map p.subtype p' ≤ range p.subtype)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M₂
⊢ f ((ofBijective f h).symm x) = x

Tactic:
by
  rw [← ofBijective_apply f (hf := h) ((ofBijective f h).symm x), apply_symm_apply]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ s • N = ⨆ a ∈ s, a • N

Tactic:
refine Eq.trans (congrArg sInf ?_) csInf_Ici
  simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]
  exact Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ a • N
⊢ p x hx

Tactic:
simp_all only [← Submodule.singleton_set_smul]

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
⊢ p x hx
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set M)
⊢ span R (⋃₀ s) = sSup (span R '' s)

Tactic:
refine le_antisymm ?_ (sSup_le fun P ⟨t, ht, h⟩ ↦ h ▸ span_mono (subset_sUnion_of_mem ht))

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set M)
⊢ span R (⋃₀ s) ≤ sSup (span R '' s)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ p ⊔ span R s = span R ↑p ⊔ span R s

Tactic:
p.span_eq

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ p ⊔ span R s = p ⊔ span R s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ span R s ⊔ p = span R s ⊔ span R ↑p

Tactic:
p.span_eq

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ span R s ⊔ p = span R s ⊔ p
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
this : Nonempty ↑s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists,
    exists_prop]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R ↑p ⊔ span R ↑p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
← span_union

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (x y_1 : M), x ∈ R ∙ y → y_1 ∈ R ∙ y → (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

Tactic:
rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
a b : R
⊢ ∃ a_1, a_1 • y = a • y + b • y
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this : Finite ↑t
⊢ sSup t ∈ s

Tactic:
have := ht'.to_subtype

Goal state after:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ sSup t ∈ s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ sSupIndep (range t)

Tactic:
rw [sSupIndep_iff]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep Subtype.val
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
r : R
⊢ (algebraMap R A) r • m ∈ span R X

Tactic:
simpa [algebraMap_smul] using smul_mem _ r hm

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
refine ⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩

Goal state after:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∀ z ∈ S, z ≤ sSup S
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∀ c ⊆ Iio k, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ Iio k, ∀ z ∈ c, z ≤ ub

Tactic:
· intro S SC cC I _
    by_cases hS : S.Nonempty
    · refine ⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩
      intro; apply le_sSup
    exact
      ⟨b, lt_of_le_of_ne hbk H, by
        simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
          forall_prop_of_false, not_false_iff]⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
s : Finset ι
inst✝ : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun i ↦ f i) s.val
⊢ a ∣ f x

Tactic:
exact h x hx

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
s : Finset ι
inst✝ : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
y : R
hy : y ∈ Multiset.map (fun i ↦ f i) s.val
⊢ a ∣ y

Tactic:
rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
this : Injective (comap f)
⊢ (comap f p ≠ ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = ⊤) ↔ p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤

Tactic:
← comap_top f,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
this : Injective (comap f)
⊢ (comap f p ≠ comap f ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = comap f ⊤) ↔
    p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case inr
ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
this : f i = ∏ j ∈ s, if i = j then f i else 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
⊢ (map f (a :: s)).prod ≤ (map g (a :: s)).prod

Tactic:
simp only [map_cons, prod_cons]
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    apply mul_le_mul
    · apply h
      simp
    · grind
    · grind [prod_nonneg]
    · apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
ha : f a ≠ 0
⊢ f a = f a ∧ f a ≠ 0

Tactic:
exact ⟨rfl, ha⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
h : (mapDomain f x) b ≠ 0
⊢ b ∈ Set.range f

Tactic:
contrapose! h; exact mapDomain_of_notMem_range _ _ h

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

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (single a m).extendDomain = single (↑a) m

Tactic:
ext a'
  obtain rfl | ha := eq_or_ne a' a.val <;>
    simp [*, a.prop, single, Pi.single, Function.update, Subtype.ext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ (fun i ↦ single i 1) '' s ⊆ ↑(supported R R s)

pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
· rintro _ ⟨_, hp, rfl⟩
    exact single_mem_supported R 1 hp

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i ↦ single i 1) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
ext i n

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
i : ι
n : ↥N
⊢ (mulLeftMap N m ∘ₗ lsingle i) n = (N.mulRightMap m ∘ₗ lsingle i) n
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s

Tactic:
exact hs hx

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
F : ↥(supported M R s) ≃ (↑s →₀ M) := restrictSupportEquiv s M
this : ⇑F = ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
⊢ IsLinearMap R ⇑F

Tactic:
rw [this]

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
F : ↥(supported M R s) ≃ (↑s →₀ M) := restrictSupportEquiv s M
this : ⇑F = ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
⊢ IsLinearMap R ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Iio a) = Iio ↑a

Tactic:
rw [← attachFin_Iio, map_valEmbedding_attachFin]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i // ¬i ∈ Set.range ⇑e }
i : Fin (n + 1)
⊢ ((embeddingFinSucc n ι).symm f) i = Fin.cons (↑f.snd) (⇑f.fst) i

Tactic:
exact Fin.cases rfl (fun j ↦ rfl) i

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = (↑i + ↑i + 1 - (n + 1 + 1)) % (n + 1 + 1)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
c : R
x : M
this : IsTorsionFree R M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0

Tactic:
exact smul_eq_zero

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x y z : ℕ∞
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

pp: case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝

Tactic:
· rcases lt_trichotomy x 1 with x_0 | rfl | x_2
    · simp only [Order.lt_one_iff.1 x_0, zero_mul, zero_epow_top]
    · simp only [one_mul, one_epow]
    · rcases lt_trichotomy y 1 with y_0 | rfl | y_2
      · simp only [Order.lt_one_iff.1 y_0, mul_zero, zero_epow_top]
      · simp
      · rw [epow_top x_2, epow_top y_2, mul_top top_ne_zero]
        exact epow_top (one_lt_mul x_2.le y_2)

Goal state after:
case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ 0 ^ (y * z) = 0 ^ z

Tactic:
zero_epow z_0,

Goal state after:
case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ 0 ^ (y * z) = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ cons x f 0 * ∏ i, cons x f i.succ = x * ∏ i, f i

Tactic:
cons_zero,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ x * ∏ i, cons x f i.succ = x * ∏ i, f i