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

Goal state before:
pp: R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑(f * f⁻¹) x = x

Tactic:
mul_inv_cancel

Goal state after:
R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑1 x = x
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective ⇑f.rangeRestrict

Tactic:
by
  rw [← range_eq_top, range_rangeRestrict]

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
s : Set (Submodule R M)
⊢ span R (⋃ S ∈ s, ↑S) = sSup s

Tactic:
by
  simpa using (Submodule.gi R M).l_sSup_u_image s

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a : α
ha : IsCoatom a
hab : a ≤ ⊤
⊢ ⊤ ≠ a

Tactic:
exact ha.ne_top.symm

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
s : Set M
y : M
⊢ x ∈ span R (insert y s) ↔ ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
simp [span_insert, mem_sup, mem_span_singleton, eq_comm (a := x)]

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
w x y z : M
⊢ (∃ a z_1, (∃ a b, a • y + b • z = z_1) ∧ w = a • x + z_1) ↔ ∃ a b c, a • x + b • y + c • z = w

Tactic:
refine exists_congr fun a ↦ ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
a : R
⊢ (∃ z_1, (∃ a b, a • y + b • z = z_1) ∧ w = a • x + z_1) → ∃ b c, a • x + b • y + c • z = w

case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
a : R
⊢ (∃ b c, a • x + b • y + c • z = w) → ∃ z_1, (∃ a b, a • y + b • z = z_1) ∧ w = a • x + z_1
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
⊢ (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) = S

Tactic:
have h : ∀ a ∈ Subtype.val '' S, IsAtom a := by
      rintro a ⟨a', ha', rfl⟩
      exact a'.prop

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
h : ∀ a ∈ Subtype.val '' S, IsAtom a
⊢ (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) = S
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ R ∙ x

Tactic:
exact Submodule.mem_span_singleton_self x

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ a • y + z + -a • y ∈ span R s

Tactic:
by simp [hz, add_assoc]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.inf' ht id ⊔ u.inf' hu id ∈ infClosure s

Tactic:
inf'_sup_inf'

Goal state after:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2) ∈ infClosure s
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✝² : MulAction A M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R A M
r : R
x : M
⊢ (algebraMap R A) r • x = r • x

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Goal state after:
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
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ span S (range ⇑(inclusion h₁)) = ⊤

Tactic:
apply map_injective_of_injective q.injective_subtype

Goal state after:
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
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ map q.subtype (span S (range ⇑(inclusion h₁))) = map q.subtype ⊤
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
ι : Sort u_8
p : ι → Submodule R M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, p i
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
by
  rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
  exact AddSubmonoid.iSup_induction (x := x) _ hx mem zero add

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Multiset ι
f g : ι → R
⊢ (map (fun i ↦ f i + g i) s).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum

Tactic:
refine s.induction_on ?_ fun a s ih ↦ ?_
  · simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]
  · simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a),
      mul_left_comm (g a), sum_map_add, antidiagonal_cons, Prod.map_fst, Prod.map_snd,
      id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]
    exact add_comm _ _

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ (a ::ₘ s).antidiagonal = map (fun t ↦ (a ::ₘ s - t, t)) (a ::ₘ s).powerset

Tactic:
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
      id, sub_cons, erase_cons_head]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ (s - x, a ::ₘ x)) s.powerset + map (fun x ↦ (a ::ₘ (s - x), x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support = {a ∈ s | f a ≠ 0}

Tactic:
dsimp [onFinset]

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ onFinsetSupport s f = {a ∈ s | ¬f a = 0}
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ ∀ x ∈ insert a s, ¬a < x

Tactic:
exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, fun i hi => (ha i hi).not_gt⟩

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

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

Tactic:
by
  simp [single_apply_eq_zero]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0

Tactic:
by
  simp [single_apply_eq_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v ↦ if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
by
  dsimp [Finsupp.prod]
  rw [f.support.prod_ite_eq']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum
⊢ single a✝ (a + s.sum) = (Multiset.map (single a✝) (a ::ₘ s)).sum

Tactic:
single_add,

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum
⊢ single a✝ a + single a✝ s.sum = (Multiset.map (single a✝) (a ::ₘ s)).sum
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : 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
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
classical
  rcases lt_or_ge (f i) 0 with hf | hf
  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind

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 : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, x b = 0
i : β
hi : i ∈ ↑x.support
⊢ i ∈ Set.range f

Tactic:
by_contra hc

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, x b = 0
i : β
hi : i ∈ ↑x.support
hc : i ∉ Set.range f
⊢ False
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ support 0 | p x} = ∅

Tactic:
support_zero,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ ∅ | p x} = ∅
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f f' : α →₀ M
a✝ : α
⊢ (mapDomain (fun x ↦ g • x) (f + f')) a✝ = (mapDomain (fun x ↦ g • x) f + mapDomain (fun x ↦ g • x) f') a✝

Tactic:
simp [mapDomain_add]

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:
refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm

Goal state after:
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)

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.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
⊢ s ∩ mulSupport f = ↑hs.toFinset ∩ mulSupport f

Tactic:
by rw [hs.coe_toFinset]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
by
  rw [← preimage_addNat_Icc_addNat, image_preimage_eq_of_subset]
  exact Icc_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (p.1 * n + ↑p.2) / n = p.1

Tactic:
rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k

pp: case s
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Finset α

pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑?s

Tactic:
· rw [Finset.prod_image']
    exact fun _ _ ↦ rfl

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑(Finset.image f s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a

Tactic:
mul_finsum

Goal state after:
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ ∑ᶠ (a : α), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (a - b).rev = a.rev + b

Tactic:
rev_eq_iff,

Goal state after:
n : ℕ
a b : Fin n
⊢ a - b = (a.rev + b).rev
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
ha : ↑a + 1 < n
⊢ ↑a < (↑a + 1 % n) % n

Tactic:
Nat.add_mod_mod,

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin n
ha : ↑a + 1 < n
⊢ ↑a < (↑a + 1) % n
Module: Mathlib.LinearAlgebra.Basis.Basic

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
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩

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
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_1
x y : ℕ∞
h : x ≠ 0
⊢ x ^ y ≠ 0

Tactic:
exact (epow_pos h).ne'

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

Goal state before:
pp: case refine_1
x y : ℕ∞
h : x ^ y = 0
⊢ x = 0

pp: case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False

Tactic:
· contrapose! h
    exact (epow_pos h).ne'

Goal state after:
case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False
Module: Mathlib.Data.ENat.Pow

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

Tactic:
rw [zero_epow y_0.ne.symm, zero_mul]

Goal state after:
case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (⊤ + z) = x ^ ⊤ * x ^ z

Tactic:
rw [top_add, epow_top x_2, top_mul]
      exact (epow_pos x_2.ne_zero).ne'

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
⊢ f x✝ = g x✝

Tactic:
by
        classical
        refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
        · rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
        · contrapose hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.2]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 3 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2

Tactic:
prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 3 → M
⊢ (∏ i, f i.castSucc) * f (last 2) = f 0 * f 1 * f 2
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 4 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3

Tactic:
prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 4 → M
⊢ (∏ i, f i.castSucc) * f (last 3) = f 0 * f 1 * f 2 * f 3
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 5 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4

Tactic:
prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 5 → M
⊢ (∏ i, f i.castSucc) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 6 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Tactic:
prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 6 → M
⊢ (∏ i, f i.castSucc) * f (last 5) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 7 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 7 → M
⊢ (∏ i, f i.castSucc) * f (last 6) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ (∏ i, f i.castSucc) * f (last 7) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ g₁ i * ↑(w i) = g₂ i * ↑(w i)

Tactic:
refine hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i✝ i : ι
hi : i ∉ s
⊢ g₁ i • ↑(w i) = g₂ i • ↑(w i)

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ ∑ i ∈ s, (g₁ i • ↑(w i)) • v i = ∑ i ∈ s, (g₂ i • ↑(w i)) • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ hv.repr.ker = ⊥

Tactic:
rw [LinearIndependent.repr, LinearEquiv.ker]

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

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

Tactic:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_eq h

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ s = t

Tactic:
have h_surj : Surjective f := by
    apply surjective_of_linearIndependent_of_span hs f _
    convert! hst <;> simp [f, comp_def]

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
h_surj : Surjective ⇑f
⊢ s = t
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := ⋯
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m ∣ ↑c * (↑b - ↑a)

Tactic:
rw [Int.mul_sub]

Goal state after:
case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m ∣ ↑c * ↑b - ↑c * ↑a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

Tactic:
rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]

Goal state after:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j, n (Fin.castLE ⋯ j) = 0