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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ f₁ + f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
apply le_trans _ (inf_comap_le_comap_add qₗ f₁ f₂)
    rw [le_inf_iff]
    exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ⇑f
x : ↥f.srange
x' : M
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'

Tactic:
h x'

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ⇑f
x : ↥f.srange
x' : M
hx' : f x' = ↑x
⊢ f x' = f x'
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g ⇑f
x : ↥(srange f)
x' : R
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'

Tactic:
h x'

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g ⇑f
x : ↥(srange f)
x' : R
hx' : f x' = ↑x
⊢ f x' = f x'
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalRing R
inst✝ : NonUnitalRing S
s t : NonUnitalSubring R
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g ⇑f
x : ↥f.range
x' : R
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'

Tactic:
h x'

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonUnitalRing R
inst✝ : NonUnitalRing S
s t : NonUnitalSubring R
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g ⇑f
x : ↥f.range
x' : R
hx' : f x' = ↑x
⊢ f x' = f x'
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.range
x' : R
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'

Tactic:
h x'

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.range
x' : R
hx' : f x' = ↑x
⊢ f x' = f x'
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
x : M
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
⊢ Irreducible (f x) ↔ Irreducible x

Tactic:
by
  simp [_root_.irreducible_iff, (EquivLike.surjective f).forall, ← map_mul, -isUnit_map_iff]

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.subtype.range = p

Tactic:
simpa using map_comap_subtype p ⊤

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g✝ : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h✝ : M₂ →ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
g : M₂ → M
h : LeftInverse g ⇑f
x : ↥f.range
x' : M
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'

Tactic:
h x'

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g✝ : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h✝ : M₂ →ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
g : M₂ → M
h : LeftInverse g ⇑f
x : ↥f.range
x' : M
hx' : f x' = ↑x
⊢ f x' = f x'
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (↑x ⊔ b) ≤ a ⊓ (b ⊔ ↑y)

Tactic:
sup_comm b

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (↑x ⊔ b) ≤ a ⊓ (↑y ⊔ b)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a : α
⊢ Ioi a = {⊤} ↔ IsCoatom a

Tactic:
by
  simp [IsCoatom, superset_antisymm_iff, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x, (x ∉ K ∧ x ∈ H) ∧ H ≠ L)

Tactic:
and_comm,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ ∃ x, H ≠ L ∧ x ∉ K ∧ x ∈ H)
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → ((H ≠ L ∧ ∃ x ∈ H, x ∉ K) ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)

Tactic:
and_comm,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → True
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x, (x ∉ H ∧ x ∈ L) ∧ H ≠ K)

Tactic:
and_comm,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x, H ≠ K ∧ x ∈ L ∧ x ∉ H)
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
r : Rˣ
⊢ R ∙ r • x = R ∙ x

Tactic:
exact span_singleton_group_smul_eq R r x

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
α : ι → Type u_5
inst✝ : CommMonoidWithZero M₀
s : Finset ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ ((↑s).pi t).indicator 1 f = ∏ i ∈ s, (t i).indicator 1 (f i)

Tactic:
classical simp [Set.indicator, prod_boole]

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
⊢ ⇑f = 1 ↔ f = 1

Tactic:
constructor
  · intro h
    simp [DFunLike.ext_iff, h]
  · intro h
    simp [h]

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
⊢ ⇑f = id ↔ f = 1

Tactic:
constructor
  · intro h
    simp [DFunLike.ext_iff, h]
  · intro h
    simp [h]

Goal state after:
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 : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
a : α
⊢ a ∈ Finset.image f ((insert i (t.preimage f hf)).erase i) ↔ a ∈ t

Tactic:
simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
a : α
⊢ (∃ a_1, (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) ↔ ¬a = ⊥ ∧ a ∈ s
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (a ::ₘ ⟦l⟧).antidiagonal =
    map (Prod.map id (cons a)) (antidiagonal ⟦l⟧) + map (Prod.map (cons a) id) (antidiagonal ⟦l⟧)

Tactic:
by
    simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
      map_coe, antidiagonal_coe', coe_add]
    rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)] <;> simp

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

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

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

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

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a ≤ ⊥

Tactic:
apply le_trans (le_inf _ hac) hc.disjoint.le_bot

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a ≤ ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩
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₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
⊢ comap f (map f p ⊔ q) = p

Tactic:
refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
⊢ x ∈ p
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ s.mulIndicator f x * sᶜ.mulIndicator g x = g x

Tactic:
Set.mulIndicator_of_notMem h,

Goal state after:
case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ 1 * sᶜ.mulIndicator g x = g x
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, ((-1) ^ #t * ∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i

Tactic:
by
  simp [sub_eq_neg_add, prod_add, prod_neg, mul_right_comm]

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

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ (x, g x) ∈ g.graph

Tactic:
exact mk_mem_graph _ (hsup ▸ hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' ↑x.support
⊢ (mapDomain f x) b = 0

Tactic:
rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' ↑x.support
⊢ ∀ x_1 ∈ x.support, (single (f x_1) (x x_1)) b = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
⊢ (mapDomain (⇑f) x) a = x (f.symm a)

Tactic:
by
  conv_lhs => rw [← f.apply_symm_apply a]
  exact mapDomain_apply f.injective _ _

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
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
| embDomain { toFun := f, inj' := hf } (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)

Tactic:
embDomain_eq_mapDomain

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
| mapDomain (⇑{ toFun := f, inj' := hf }) (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case ha
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ 0 ≤ ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2

Tactic:
exact sq_nonneg _

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

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

Tactic:
obtain rfl | ha := eq_or_ne a' a.val

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

case inr
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : a' ≠ ↑a
⊢ (single a m).extendDomain a' = (single (↑a) m) a'
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x✝ : α →₀ M
a✝ : β
⊢ (embDomain f x✝) a✝ = (mapDomain (⇑f) x✝) a✝

Tactic:
embDomain_eq_mapDomain

Goal state after:
case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x✝ : α →₀ M
a✝ : β
⊢ (mapDomain (⇑f) x✝) a✝ = (mapDomain (⇑f) x✝) a✝
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Tactic:
by
  rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]
  simpa only [inter_comm] using disjoint_sdiff_inter t s

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

Goal state before:
pp: case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Tactic:
rw [notMem_mulSupport.mp ha]
    exact one_dvd (finprod f)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
        simpa only [hs.mem_toFinset]

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
by
  rw [Set.sUnion_eq_biUnion]
  exact finprod_mem_biUnion h ht₀ ht₁

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
⊢ vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1) = vecCons b (vecCons a x)

Tactic:
by
  ext j : 1
  match j with
  | 0 => simp
  | 1 => simp
  | ⟨i + 2, h⟩ =>
    have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = Fin.succ (Fin.succ ⟨i, by lia⟩) := by grind
    simp only [Nat.succ_eq_add_one, h', Function.comp_apply,
      Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero _) (Fin.succ_succ_ne_one _), cons_val_succ]

Goal state after:
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:
zero_epow y_0.ne.symm,

Goal state after:
case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 * 0 ^ z
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:
by
  rw [prod_univ_castSucc, prod_univ_seven]
  rfl

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m n, m • p + a = n • p + b) → ∃ m, m • p = b - a

Tactic:
rintro ⟨m, n, h⟩
    use m - n
    rw [sub_zsmul, ← sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm b]
    exact mod_cast h

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j with i ≤ j.castSucc, f i j) * ∏ i, ∏ j with j.castSucc < i, f i j =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j

Tactic:
rw [Fin.prod_univ_castSucc, Fin.prod_univ_succ]

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ((∏ i, ∏ j with i.castSucc ≤ j.castSucc, f i.castSucc j) * ∏ j with last n ≤ j.castSucc, f (last n) j) *
      ((∏ j with j.castSucc < 0, f 0 j) * ∏ i, ∏ j with j.castSucc < i.succ, f i.succ j) =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (f : Fin n → Fin m), ∑ i, ↑(f i) * m ^ ↑i < m ^ n
f : Fin (n + 1) → Fin m
⊢ ∑ i, ↑(f i) * m ^ ↑i < m ^ (n + 1)

Tactic:
cases m

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
ih : ∀ (f : Fin n → Fin 0), ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ n
f : Fin (n + 1) → Fin 0
⊢ ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ (n + 1)

case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ (n + 1)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
⊢ i.Maximal

Tactic:
w

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
⊢ LinearIndependent R Subtype.val → range v ⊆ w → range v = w
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : n ≤ b
⊢ a ≡ b - n [MOD n] ↔ a ≡ b [MOD n]

Tactic:
← modEq_add_modulus_iff,

Goal state after:
n a b : ℕ
h : n ≤ b
⊢ a ≡ b - n + n [MOD n] ↔ a ≡ b [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
⊢ Disjoint (span R (range v)) ⊥

Tactic:
disjoint_bot_right

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

Goal state before:
pp: case refine_1.refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
⊢ f i = 0

pp: case refine_1.refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
· simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)

Goal state after:
case refine_1.refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
⊢ Disjoint (span R (Set.range v)) ⊥

Tactic:
disjoint_bot_right

Goal state after: