mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ f.range ≤ ⊥ ↔ f = 0

Tactic:
by
  rw [range_le_iff_comap]; exact ker_eq_top

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:
simpa using (map_le_range : map p.subtype p' ≤ range p.subtype)

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 p' : Submodule R M
⊢ map p.subtype ⊤ ≤ p' ↔ p ≤ p'

Tactic:
by rw [map_subtype_top]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y, O.subtype y ∈ N ∧ ϕ y = x

Tactic:
rintro ⟨y, yO, yN, h⟩
    exact ⟨⟨y, yO⟩, yN, h⟩

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 M
⊢ span R (s \ {0}) = span R s

Tactic:
by_cases h : 0 ∈ s
  · rw [← span_insert_zero, show insert 0 (s \ {0}) = s by simp [h]]
  · simp [h]

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 M
p : (x : M) → x ∈ span R s → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
let p : Submodule R M :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩ }
  exact span_le (p := p) |>.mpr (fun y hy ↦ ⟨subset_span hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ a ⊓ b

Tactic:
apply le_inf inf_le_left

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ b
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
by
    simp_rw [Set.Iic.isCompl_iff]
    obtain ⟨y, hdisjoint, rfl⟩ := exists_disjoint_and_sup_eq hx
    exact ⟨⟨y, le_sup_right⟩, hdisjoint, rfl⟩

Goal state after:
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 : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∀ (x y : M),
    x ∈ span R (↑p ∪ ↑p') →
      y ∈ span R (↑p ∪ ↑p') →
        (∃ y ∈ p, ∃ z ∈ p', y + z = x) → (∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y) → ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = x + y

Tactic:
rintro _ _ - - ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by
        rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a : α
ha : a ∈ latticeClosure s
b : α
hb : b ∈ latticeClosure s
⊢ f a ⊔ f b ∈ f '' latticeClosure s

Tactic:
exact ⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
⊢ (s.attach.SupIndep fun a ↦ f ↑a) ↔ s.SupIndep f

Tactic:
by
  simpa [Finset.attach_map_val] using! (supIndep_map (s := s.attach) (g := .subtype _)).symm

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
suffices ∀ (s : Finset ι) (hst : Disjoint ↑s t), Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i) by
    specialize this hs.toFinset
    aesop

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
⊢ ∀ (s : Finset ι), Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
⊢ ∀ (s : Finset ι), Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
intro s

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
⊢ Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
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:
Algebra.algebraMap_eq_smul_one,

Goal state after:
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
⊢ (r • 1) • x = r • x
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ x • 1 = (x • 1) • 1
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
⊢ IsSupClosedCompact α

Tactic:
intro s

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
⊢ s.Nonempty → SupClosed s → sSup s ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)

Tactic:
intro s

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
⊢ ↑s ⊆ f '' {j | j ≠ i} → Disjoint (f i) (s.sup id)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)

Tactic:
intro s

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
⊢ ↑s ⊆ f '' {j | j ≠ i} → Disjoint (f i) (s.sup id)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ iSupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
iSupIndep_iff_supIndep

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
intro s

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
induction s using Finset.strongInduction with
  | H s ih =>
    by_cases hs : 1 < s.card; swap
    · by_cases hcard0 : s.card = 0 <;> grind [Finset.card_eq_zero, Finset.card_eq_one]
    · obtain ⟨k₁, k₂, _, _, h⟩ := Finset.one_lt_card_iff.mp hs
      obtain ⟨i, hi⟩ : ∃ i : ι, k₁ i ≠ k₂ i := Function.ne_iff.mp h
      classical
      rw [← Finset.image_biUnion_filter_eq s (· i)]
      refine Finset.SupIndep.biUnion ?_ (by grind)
      apply ((h_indep i).supIndep' _).mono
      simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
      rintro _ _ _ _ rfl
      exact iInf_le _ _

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

Goal state before:
pp: case inl
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p < p'
h : p ⊓ f.ker < p' ⊓ f.ker
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

pp: case inr
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p < p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
· simpa [inf_comm] using Or.inr h

Goal state after:
case inr
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p < p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ {g | ∀ (i : α), g i ∈ Set.range e} = Set.univ

Tactic:
he.range_eq

Goal state after:
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ {g | ∀ (i : α), g i ∈ Set.univ} = Set.univ
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (embDomain Embedding.some f).some = f

Tactic:
by
  ext; rw [some_apply]; exact embDomain_apply_self _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ (mulSupport fun x ↦ ⨆ i, f i x) ⊆ ⋃ i, mulSupport (f i)

Tactic:
simp only [mulSupport_subset_iff', mem_iUnion, not_exists, notMem_mulSupport]
  intro x hx
  simp only [hx, ciSup_const]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : a ∉ f.support
⊢ g a (f a) = 1

Tactic:
simp only [notMem_support_iff] at h
    rw [h]
    exact h₁ h

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ s.card ≤ s.prod

Tactic:
rw [← Multiset.prod_replicate, ← Multiset.map_const]
  exact prod_map_le_prod _ h

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

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (List.map (fun i ↦ min (f i) (g i)) l).prod ≤ min (List.map f l).prod (List.map g l).prod

Tactic:
apply List.prod_min_le

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
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ (head :: tail).prod

Tactic:
simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)

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
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
⊢ (s.support.biUnion fun x ↦ {f x}) ⊆ image f s.support

Tactic:
rw [Finset.biUnion_singleton]

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

Goal state before:
pp: case pos
α : 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
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : p a
⊢ a ∈ Finset.filter p f.support ↔ f a ≠ 0

Tactic:
simp only [h, mem_filter, mem_support_iff]
        tauto

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

Goal state before:
pp: case neg
α : 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
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
⊢ a ∈ Finset.filter p f.support ↔ 0 ≠ 0

Tactic:
simp only [h, mem_filter, mem_support_iff]
        tauto

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
c : R
⊢ c • b.repr.symm (single i 1) = c • b i

Tactic:
repr_symm_single_one

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
c : R
⊢ c • b i = c • b i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
v : Option α → M
f : Option α →₀ R
⊢ (linearCombination R v) f = f none • v none + (linearCombination R (v ∘ Option.some)) f.some

Tactic:
by
  rw [linearCombination_apply, sum_option_index_smul, linearCombination_apply]; simp

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

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

Tactic:
rw [← preimage_addNat_Ico_addNat, image_preimage_eq_of_subset]
  exact Ico_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_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ x✝ : M
⊢ f (x✝¹ + x✝) i = f x✝¹ i + f x✝ i

Tactic:
by rw [hadd, Pi.add_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
h' : ∀ x ∈ s, f x = 1
⊢ False

Tactic:
exact h (finprod_mem_of_eqOn_one h')

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

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

Tactic:
refine Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
    dsimp only
    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.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α : Type u_1
m n : ℕ
f : Fin (m + n) → α
⊢ (fun fg ↦ append fg.1 fg.2) ((fun f ↦ (fun i ↦ f (castAdd n i), fun i ↦ f (natAdd m i))) f) = f

Tactic:
by simp [Fin.append_castAdd_natAdd]

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 α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f

Tactic:
refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop

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

Goal state before:
pp: case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
epow_top (x_2.trans_le x_z)

Goal state after:
case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ ⊤
Module: Mathlib.Data.ENat.Pow

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

Tactic:
mul_top top_ne_zero

Goal state after:
case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = ⊤
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, snoc f x i = (∏ i, f i) * x

Tactic:
simp [prod_univ_castSucc]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ f 0 = 0

Tactic:
simp [f]

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

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ (l * n) • p + n • b = l • n • p + n • b

Tactic:
mul_nsmul'

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ l • n • p + n • b = l • n • p + n • b
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
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G 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 : ι → G
⊢ ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i

Tactic:
intro s

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G 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 : ι → G
s : Finset ι
⊢ ∀ (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i
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 ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i

Tactic:
intro s

Goal state after:
ι : 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 ι
⊢ ∀ (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mp
a b n : ℕ
⊢ (∃ m n_1, m • n + a = n_1 • n + b) → a % n = b % n

Tactic:
rintro ⟨k, l, h⟩

Goal state after:
case mp
a b n k l : ℕ
h : k • n + a = l • n + b
⊢ a % n = b % n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat a = Int.ofNat b

Tactic:
rw [eq_comm, ← sub_eq_zero]

Goal state after:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat b - Int.ofNat a = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
have hmd := gcd_dvd_left m c

Goal state after:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
⊢ a ≡ b [MOD m / m.gcd c]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑a + ↑n * n.gcdA m * (↑b - ↑a) / ↑(n.gcd m))

pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑(n.gcd m) ∣ ↑(n.gcd m) * ↑a

Tactic:
Int.mul_ediv_assoc _ h.dvd,

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑a + ↑n * n.gcdA m * ((↑b - ↑a) / ↑(n.gcd m)))

case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑(n.gcd m) ∣ ↑(n.gcd m) * ↑a