mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ span S (range ⇑(inclusion h₁)) = ⊤

Tactic:
by
  suffices (span S (range (inclusion h₁))).map q.subtype = q by
    apply map_injective_of_injective q.injective_subtype
    rw [this, q.map_subtype_top]
  rw [map_span]
  suffices q.subtype '' ((LinearMap.range (inclusion h₁)) : Set <| q.restrictScalars R) = p by
    refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) h₁
  ext x
  simpa [range_inclusion] using fun hx ↦ h₁ hx

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

Goal state before:
pp: case mp
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
⊢ ∃ z, z • a • y = y

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Goal state after:
case mp.inl
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
a b : R
hb : b • a • 0 = 0
⊢ ∃ z, z • a • 0 = 0

case mp.inr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ z, z • a • y = y
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x y : M
⊢ (∃ z, z • x = y) → R ∙ x = R ∙ y

Tactic:
rintro ⟨u, rfl⟩
    exact (span_singleton_group_smul_eq _ _ _).symm

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

Goal state before:
pp: case refine_4.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • 0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
rw [smul_zero]
      exact AddSubmonoid.zero_mem _

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
j : ι
| φ' j (mulSingle i m j)

Tactic:
Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
j : ι
| mulSingle i (φ' i m) j
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s ∪ s).mulIndicator f = t.mulIndicator f

pp: case h
α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s

Tactic:
sdiff_union_self,

Goal state after:
α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t ∪ s).mulIndicator f = t.mulIndicator f

case h
α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ ∃ c, ∃ z ∈ s, c • x + z = y

Tactic:
simpa [mem_sup, mem_span_singleton] using hqp.le hyq

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ toSpanSingleton R M x = toSpanSingleton R M 0 ↔ x = 0

Tactic:
(toSpanSingleton_injective R M).eq_iff

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ x = 0 ↔ x = 0
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ single a b = 0 ↔ b = 0

Tactic:
simp [DFunLike.ext_iff, single_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (single f₁ g₁).support ∪ (single f₂ g₂).support = {f₁, f₂}

pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Disjoint (single f₁ g₁).support (single f₂ g₂).support

Tactic:
support_single _ hg₁,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ {f₁} ∪ (single f₂ g₂).support = {f₁, f₂}

ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Disjoint (single f₁ g₁).support (single f₂ g₂).support
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ l d = (single c b) d

Tactic:
rw [← embDomain_apply_self f l, h]

Goal state after:
case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ (single a b) (f d) = (single c b) d
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.biUnion fun x ↦ (f x).support

Tactic:
by
  rw [← Finset.sup_eq_biUnion]
  induction s using Finset.cons_induction_on with
  | empty => rfl
  | cons _ _ _ ih =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
⊢ (if x * y = 0 then 0 else 1) = (if x = 0 then 0 else 1) * if y = 0 then 0 else 1

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Goal state after:
case inr.inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ (if x * 0 = 0 then 0 else 1) = (if x = 0 then 0 else 1) * if 0 = 0 then 0 else 1

case inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x * y = 0 then 0 else 1) = (if x = 0 then 0 else 1) * if y = 0 then 0 else 1
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Goal state after:
case inr.inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ (if x + 0 = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if 0 = 0 then 0 else 1

case inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
⊢ Injective graph

Tactic:
intro f

Goal state after:
α : Type u_12
M : Type u_13
inst✝ : Zero M
f : α →₀ M
⊢ ∀ ⦃a₂ : α →₀ M⦄, f.graph = a₂.graph → f = a₂
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s : Multiset (α →₀ M)
a : α
⊢ ∀ (a_1 : α →₀ M) (s : Multiset (α →₀ M)),
    (a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support) → a ∈ (a_1 ::ₘ s).sum.support → ∃ f ∈ a_1 ::ₘ s, a ∈ f.support

Tactic:
intro f

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s : Multiset (α →₀ M)
a : α
f : α →₀ M
⊢ ∀ (s : Multiset (α →₀ M)),
    (a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support) → a ∈ (f ::ₘ s).sum.support → ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i

Tactic:
← h2i,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ insert i s, f j ≤ ∏ j ∈ t, f j

Tactic:
apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝³ : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝² : Fintype η
ιs✝ : η → Type u_14
inst✝¹ : Zero α✝
α : Type u_15
ιs : η → Type u_16
inst✝ : AddMonoid α
f g : (j : η) × ιs j →₀ α
⊢ sigmaFinsuppEquivPiFinsupp.toFun (f + g) = sigmaFinsuppEquivPiFinsupp.toFun f + sigmaFinsuppEquivPiFinsupp.toFun g

Tactic:
by
      ext
      simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ a ∈ (b • g).support → a ∈ g.support

Tactic:
by
  simp only [smul_apply, mem_support_iff, Ne]
  exact mt fun h => h.symm ▸ smul_zero _

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case refine_1
α : Type u_2
s : Finset α
f : α → ℕ
h : ∑ x ∈ s, f x ≤ 1
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
⊢ x = y ∧ f x = 1

pp: case refine_2
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
⊢ ∑ x ∈ s, f x ≤ 1

Tactic:
· replace h := (sum_mono_set f (show {x, y} ⊆ s by grind)).trans h
    grind

Goal state after:
case refine_2
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
⊢ ∑ x ∈ s, f x ≤ 1
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
x✝ : M
⊢ (lapply a ∘ₗ lsingle a') x✝ = 0 x✝

Tactic:
simp [h.symm]

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

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

Tactic:
by
  refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm
  · rintro _ ⟨_, hp, rfl⟩
    exact single_mem_supported R 1 hp
  · rw [← l.sum_single]
    refine sum_mem fun i il => ?_
    rw [show single i (l i) = l i • single i 1 by simp]
    exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Surjective ⇑(ringHomEndFinsupp ι)

Tactic:
intro f

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R (ι →₀ M)) (ι →₀ M)
⊢ ∃ a, (ringHomEndFinsupp ι) a = f
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (s ∩ t) = supported M R s ⊓ supported M R t

Tactic:
rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
exact Icc_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
⊢ Basis ι R' M

Tactic:
by
  letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)
  haveI : IsScalarTower R' R M :=
    { smul_assoc := fun x y z => by
        change (f.symm x * y) • z = x • (y • z)
        rw [mul_smul, ← h, f.apply_symm_apply] }
  exact ofRepr <| (b.repr.restrictScalars R').trans <|
    Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ 1

Tactic:
rw [← finprod_one (α := α)]

Goal state after:
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin m × Fin n
⊢ ↑x.2 + n * ↑x.1 + 1 = ↑x.1 * n + ↑x.2 + 1

Tactic:
ac_rfl

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 ↦ n_1 + n_1 + 1

Tactic:
by
  ext i
  simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
  cases n with
  | zero =>
    obtain ⟨i, hi⟩ := i
    simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl
  | succ n =>
    split_ifs with h <;> congr
    · simp [Nat.mod_eq_of_lt, h]
    · rw [Fin.val_mk, not_lt] at h
      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)]
      refine (Nat.mod_eq_of_lt ?_).symm
      lia

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
mem_mulSupport,

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : ¬f a ≠ 1
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ x ∉ mulSupport fun a ↦ ∏ b ∈ s, f a b

Tactic:
mem_mulSupport,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ ¬∏ b ∈ s, f x b ≠ 1
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y default) • x = c • y default • x

Tactic:
← smul_assoc

Goal state after:
case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y default) • x = (c • y default) • x
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ 0 = 1

Tactic:
pow_zero

Goal state after:
x : ℕ∞
⊢ 1 = 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ k.castSucc

Tactic:
exact le_iff_val_le_val.2 (le_of_lt h)

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
co : n.Coprime m
a b z : ℕ
hzan : z ≡ a [MOD n]
hzbm : z ≡ b [MOD m]
⊢ z ≡ ↑(chineseRemainder co a b) [MOD n * m]

Tactic:
by
  simpa [Nat.Coprime.lcm_eq_mul co] using
    mod_lcm (hzan.trans ((chineseRemainder co a b).prop.1).symm)
      (hzbm.trans ((chineseRemainder co a b).prop.2).symm)

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
lhs

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t'
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
by
  have : Disjoint {x | x ≠ a} {a} := disjoint_singleton_right.mpr <| by simp
  replace this := (Set.encard_union_eq this).symm
  have aux : {x | x ≠ a} ∪ {a} = univ := by ext x; simp [eq_or_ne x a]
  rwa [encard_singleton, aux, encard_univ] at this

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
by
  refine _root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_
  have := congr($hc r)
  simp only [RingHom.coe_comp, comp_apply] at this
  simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent R (-v)

Tactic:
intro f

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
f : ι →₀ R
⊢ ∀ ⦃a₂ : ι →₀ R⦄, (Finsupp.linearCombination R (-v)) f = (Finsupp.linearCombination R (-v)) a₂ → f = a₂
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard = 1 ↔ ∃ x, s = {x}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, hx⟩ ↦ by rw [hx, encard_singleton]⟩
  obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
  exact ⟨x, ((finite_singleton x).eq_of_subset_of_encard_le (by simpa) (by simp [h])).symm⟩

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

Goal state before:
pp: case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
a : K
ha : a • v i ∈ span K (v '' (univ \ {i}))
ha' : ¬a = 0
⊢ False

Tactic:
exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ z * ∑ a ∈ (b.repr y).support, (b.repr y) a • b a = (∑ a ∈ (b.repr y).support, (b.repr y) a • b a) * z

Tactic:
Finset.sum_mul,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ z * ∑ a ∈ (b.repr y).support, (b.repr y) a • b a = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: case inl
α : Type u_1
l : List α
h : l.Nodup
h✝ : Finite α
⊢ ↑l.length ≤ ENat.card α

Tactic:
h.length_le_natCard,

Goal state after:
case inl
α : Type u_1
l : List α
h : l.Nodup
h✝ : Finite α
⊢ ↑(Nat.card α) ≤ ENat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Tactic:
exact Nat.zero_le _

Goal state after: