mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
⊢ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

Tactic:
intro b hb
    apply ωSup_le _ _ _
    rintro i y hy
    simp only [Part.mem_ωSup] at hb
    rcases hb with ⟨j, hb⟩
    replace hb := hb.symm
    simp only [Part.eq_some_iff, Chain.coe_map, Function.comp_apply] at hy hb
    replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb
    replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy
    apply h''' (max i j)
    simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe]
    exact ⟨_, hb, hy⟩

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

Goal state before:
pp: α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T) + #↑T = #↑S

Tactic:
refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [sdiff_union_of_subset h]
  exact disjoint_sdiff_self_left

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ mk.symm c₁ • a = mk.symm c₂ • a

Tactic:
by
    rcases exists_pair_ne β with ⟨x, y, hne⟩
    contrapose! hne
    have := Classical.decEq α
    replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
    simpa [smul_apply, hne] using h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = MulOpposite.unop (MulOpposite.op (g 1)) * MulOpposite.unop (MulOpposite.op (f 1))

Tactic:
dsimp [← smul_eq_mul]; simp_rw [← map_smul, smul_eq_mul, mul_one]; rfl

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
c : ℕ
a : M
⊢ e (c • a) = c • e a

Tactic:
map_nsmul

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
c : ℕ
a : M
⊢ c • e a = c • e a
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

Tactic:
simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ t • m ∈ ⨆ a, ↑a
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ Commute (f.restrict hf) (g.restrict hg)

Tactic:
by
  change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)
  congr 1

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
      · rw [Set.image_empty, sSup_empty]
      · rw [hs.image_const, sSup_singleton]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0

Tactic:
by
  simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤)

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (⨅ a ∈ s, a.1) ⊓ ⨅ a ∈ s, a.2 = ⨅ a ∈ s, a.1 ⊓ a.2

Tactic:
iInf_inf_eq

Goal state after:
Module: Mathlib.Algebra.Ring.ULift

Goal state before:
pp: R : Type u
inst✝ : Distrib R
x✝² x✝¹ x✝ : ULift R
⊢ Equiv.ulift (x✝² * (x✝¹ + x✝)) = Equiv.ulift (x✝² * x✝¹ + x✝² * x✝)

Tactic:
by simp [left_distrib]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

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

Goal state before:
pp: case mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
n : ℕ
x✝ : n + 2 ≠ 1
⊢ ¬Irreducible (x ^ (n + 2))

Tactic:
intro ⟨h₁, h₂⟩

Goal state after:
M : Type u_2
inst✝ : Monoid M
x : M
n : ℕ
x✝ : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
⊢ False
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ b

Tactic:
induction n with
  | zero =>
    rw [pow_zero]
    exact one_dvd b
  | succ n ih =>
    obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
    rw [pow_succ]
    apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
    rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z

Tactic:
rwa [mul_right_inj' hp0] at h

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

Goal state before:
pp: M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ x✝ ∈ Submonoid.map h M₀⁰ ↔ x✝ ∈ S⁰

Tactic:
simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]

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

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

Tactic:
by rw [← mk_zero, mk_mul_mk, mul_zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
by simpa [mem_mul] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
by simpa [mem_mul] using! hs

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
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 τ₁₂ τ₂₃ τ₁₃
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : RingHomSurjective τ₂₃
inst✝ : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
⊢ (g ∘ₛₗ f).range = g.range

Tactic:
by rw [range_comp, hf, Submodule.map_top]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ SupClosed (insert a s)

Tactic:
by
  rw [SupClosed]
  have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a
  aesop

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬a ⊔ b = ⊤ ↔ a ⊔ b = a

Tactic:
exact ha.ne_top_iff_eq le_sup_left

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

Tactic:
simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall,
    OrderDual.toDual_le_toDual, and_comm, isStronglyCoatomic_iff] using forall_comm

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
⊢ i ∈ t

Tactic:
by_contra hit

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
hit : i ∉ t
⊢ False
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ IsLUB (Function.eval i '' {f | IsAtom f ∧ f ≤ s}) (s i)

Tactic:
simp_rw [isAtom_iff_eq_single]

Goal state after:
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ IsLUB (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s}) (s i)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}

Tactic:
· rintro h c ((rfl : c = a) | (rfl : c = b))
    · convert! h using 1
      simp [hab, sSup_singleton]
    · convert! h.symm using 1
      simp [hab, sSup_singleton]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))

Tactic:
sSup_image

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ a ∈ {j | j ≠ i}, t a)
Module: Mathlib.Algebra.Module.Submodule.EqLocus

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f g : M →ₛₗ[τ₁₂] M₂
r : R
x : M
hx : f x = g x
⊢ f (r • x) = g (r • x)

Tactic:
simpa only [map_smulₛₗ _] using congr_arg (τ₁₂ r • ·) hx

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
⊢ i ∈ s

Tactic:
by
  by_contra contra
  replace h₁ : Disjoint (f i) (⨆ i ∈ s, f i) := (h₁ i).mono_right <| biSup_mono <| by aesop
  aesop

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 ∈ span R (s • t)

Tactic:
apply zero_mem

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

Goal state before:
pp: case mp.inr.refine_1
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
⊢ b * a = 1

Tactic:
apply smul_left_injective R hy
      simpa only [mul_smul, one_smul]

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

Goal state before:
pp: ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle i m)
⊢ p f

Tactic:
by
  cases nonempty_fintype ι
  rw [← Finset.univ_prod_mulSingle f]
  exact Finset.prod_induction _ _ mul one (by simp [mulSingle])

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
⊢ HasFiniteMulSupport fun x ↦ 1

Tactic:
by
  simp [HasFiniteMulSupport]

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₂
S : Submodule R M
hf : Surjective ⇑f
⊢ Surjective ⇑(f.domRestrict S) ↔ Codisjoint S f.ker

Tactic:
by
  rw [← LinearMap.range_eq_top] at hf ⊢
  rw [← hf, LinearMap.range_domRestrict, map_eq_range_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
⊢ f a = g a

Tactic:
exact if h : a ∈ f.support then h₂ a h else by
        have hf : f a = 0 := notMem_support_iff.1 h
        have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
        rw [hf, hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
⊢ HasFiniteMulSupport 1

Tactic:
by
  simp [HasFiniteMulSupport]

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 : α ↪ β
v : α →₀ M
a : β
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
by_cases h : a ∈ Set.range f

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 ↔ ∃ a ∈ x.support, f a = t

Tactic:
refine ⟨?_, fun ⟨i, i_in, hi⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 → ∃ a ∈ x.support, f a = t

case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬(mapDomain f x) t = 0
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst✝² : DecidablePred p
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
v : α →₀ M
⊢ ⇑(filter p (b • v)) = ⇑(b • filter p v)

Tactic:
simp only [filter_eq_indicator, coe_smul]
    exact Set.indicator_const_smul { x | p x } b v

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 : Finset α
h : mulSupport f ⊆ ↑s
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i

Tactic:
have A : mulSupport (f ∘ PLift.down) = Equiv.plift.symm '' mulSupport f := by
    rw [mulSupport_comp_eq_preimage]
    exact (Equiv.plift.symm.image_eq_preimage_symm _).symm

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f 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 : α → M
⊢ span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(linearCombination R v)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ span R (Set.range v) = ⊤ ↔ (linearCombination R v).range = ⊤
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
⊢ b.repr.symm ((Finsupp.domLCongr e.symm) (single i' 1)) = b.repr.symm (single (e.symm i') 1)

Tactic:
Finsupp.domLCongr_single

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
⊢ b.repr.symm (single (e.symm i') 1) = b.repr.symm (single (e.symm i') 1)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(Fintype.linearCombination R v)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ span R (Set.range v) = ⊤ ↔ (Fintype.linearCombination R v).range = ⊤
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend ⋯ u v) i

Tactic:
vecAppend_eq_ite

Goal state after:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ (if h : ↑i < m + 1 then vecCons x u ⟨↑i, h⟩ else v ⟨↑i - (m + 1), ⋯⟩) =
    vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAppend ⋯ v v ⟨↑i + ↑i, ⋯⟩ = v (i + i)

Tactic:
vecAppend_eq_ite

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v ⟨↑i + ↑i, ⋯⟩ else v ⟨↑i + ↑i - n, ⋯⟩) = v (i + i)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j

Tactic:
by
  rw [← finprod_mem_univ f, ← finprod_mem_univ g]
  exact finprod_mem_eq_of_bijOn _ he₀.bijOn_univ fun x _ => he₁ x

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

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

Tactic:
simp only [Nat.mod_eq_sub_mod h]

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAppend ⋯ v v ⟨↑i + ↑i + 1, ⋯⟩ = v (i + i + 1)

Tactic:
vecAppend_eq_ite

Goal state after:
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1), ⋯⟩) = v (i + i + 1)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Tactic:
cases nonempty_fintype ι
  lift t to ι → Finset α using ht
  classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

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
s : Set α
t : Set β
f : α → β → M
hs : s.Finite
ht : t.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j

Tactic:
by
  lift s to Finset α using hs; lift t to Finset β using ht
  simp only [finprod_mem_coe_finset]
  exact Finset.prod_comm

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k < k - 1 ∨ ↑k = ↑(k - 1) ↔ k < k - 1

Tactic:
val_inj,

Goal state after:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k < k - 1 ∨ k = k - 1 ↔ k < k - 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a

Tactic:
rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]

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

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ Surjective ⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯).range = ⊤