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
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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x✝ : M
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
S : Submodule R M
x y : M
hy : y ∈ S
hxy : f y = f x
⊢ x ∈ S

Tactic:
rw [hf.eq_iff] at hxy

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
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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x✝ : M
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
S : Submodule R M
x y : M
hy : y ∈ S
hxy : y = x
⊢ x ∈ S
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
p q : Subsemiring R
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by cases p; cases q; congr; exact SetLike.coe_injective h

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
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
inst✝ : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))

Tactic:
by
  rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
p q : NonUnitalSubring R
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by cases p; cases q; congr; exact SetLike.coe_injective h

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
a : A
m : M
⊢ r • a • m = a • r • m

Tactic:
algebra_compatible_smul A r (a • m),

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
a : A
m : M
⊢ (algebraMap R A) r • a • m = a • r • m
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Submonoid.map f (algebraMapSubmonoid A M) = algebraMapSubmonoid B M

Tactic:
by
  ext x
  constructor
  · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
    simp only [AlgHom.commutes]
    use r
  · rintro ⟨r, hr, rfl⟩
    simp only [Submonoid.mem_map]
    use (algebraMap R A r)
    simp only [AlgHom.commutes, and_true]
    use r

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
S : ι → Subring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a * ↑1 = b

Tactic:
Units.val_one,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a * 1 = b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q

Tactic:
by
  rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑b

Tactic:
by simp_rw [hc, Submonoid.coe_mul, dvd_mul_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ Prime (Associates.mk p) ↔ Prime p

Tactic:
rw [Prime, _root_.Prime, forall_associated]
  simp only [forall_associated, mk_ne_zero, isUnit_mk, mk_mul_mk, mk_dvd_mk]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse ⇑g ⇑f
⊢ f.range ≤ (f ∘ₗ g - id).ker

Tactic:
by rintro y ⟨x, rfl⟩; simp [h x]

Goal state after:
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₂
hf : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ map f (p ⊔ q) = ⊤

Tactic:
codisjoint_iff.mp hpq,

Goal state after:
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₂
hf : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ map f ⊤ = ⊤
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
⊢ 0 ∈ ↑(span R s) ∧ s ⊆ ↑(span R s)

Tactic:
exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩

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

Goal state before:
pp: case refine_1
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 ∈ ↑p ∪ ↑p', ∃ y ∈ p, ∃ z ∈ p', y + z = x

pp: case refine_2
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')
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = 0

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

pp: case refine_4
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')
⊢ ∀ (a : R), ∀ x ∈ span R (↑p ∪ ↑p'), (∃ y ∈ p, ∃ z ∈ p', y + z = x) → ∃ y ∈ p, ∃ z ∈ p', y + z = a • x

Tactic:
· rintro y (h | h)
      · exact ⟨y, h, 0, by simp, by simp⟩
      · exact ⟨0, by simp, y, h, by simp⟩

Goal state after:
case refine_2
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')
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = 0

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

case refine_4
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')
⊢ ∀ (a : R), ∀ x ∈ span R (↑p ∪ ↑p'), (∃ y ∈ p, ∃ z ∈ p', y + z = x) → ∃ y ∈ p, ∃ z ∈ p', y + z = a • x
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
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) ∧ b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
and_imp,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → 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
inst✝ : OrderTop A
K : A
⊢ (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

Tactic:
and_imp,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderTop A
K : A
⊢ (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
inhabit α

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case left.inf
α : 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 ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)

Tactic:
rintro a - b - ha hb
    simpa [map_inf] using isSublattice_latticeClosure.infClosed ha hb

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊤ ≤ equivBool b ↔ ⊤ ≤ b

Tactic:
· rcases eq_bot_or_eq_top b with (rfl | rfl)
        · simp [bot_ne_top.symm, Bool.false_lt_true]
        · simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
⊢ equivBool a ≤ equivBool b ↔ a ≤ b

Tactic:
by
      rcases eq_bot_or_eq_top a with (rfl | rfl)
      · simp
      · rcases eq_bot_or_eq_top b with (rfl | rfl)
        · simp [bot_ne_top.symm, Bool.false_lt_true]
        · simp

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
⊢ Disjoint ((fun b ↦ f ⟨i, b⟩) j) (t.sup fun b ↦ f ⟨i, b⟩)

Tactic:
suffices Disjoint (f ⟨i, j⟩) ((t.image fun b ↦ ⟨i, b⟩).sup f) by simpa only [sup_image]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
⊢ Disjoint (f ⟨i, j⟩) ((image (fun b ↦ ⟨i, b⟩) t).sup f)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
⊢ Disjoint ((fun i ↦ t.sup fun i' ↦ f (i, i')) i) (u.sup fun i ↦ t.sup fun i' ↦ f (i, i'))

Tactic:
suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ (s ∪ t).SupIndep f

Tactic:
by
  rw [show s ∪ t = ({s, t} : Finset _).biUnion id by simp]
  grind [SupIndep.biUnion, supIndep_pair]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (fun i ↦ ⨆ (h : i ∈ s), ⨆ (_ : ⟨i, h⟩ ≠ ⟨a, b⟩), (f ∘ Subtype.val) ⟨i, h⟩) = fun a_1 ↦ ⨆ (_ : a_1 ∈ s.erase a), f a_1

Tactic:
simp [iSup_and, @iSup_comm _ (_ ∈ s)]

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
this : ∀ (s : Finset ι), Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
by
    specialize this hs.toFinset
    aesop

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')

Tactic:
refine le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ (p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝¹ : x ∈ t a
y : κ a
a✝ : y ∈ t a
h : x ≠ y
⊢ Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))

Tactic:
simp only [disjoint_iff_ne, mem_image]

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝¹ : x ∈ t a
y : κ a
a✝ : y ∈ t a
h : x ≠ y
⊢ ∀ (a_1 : (a' : ι) → a' ∈ insert a s → κ a'),
    (∃ a_2 ∈ s.pi t, Pi.cons s a x a_2 = a_1) →
      ∀ (b : (a' : ι) → a' ∈ insert a s → κ a'), (∃ a_3 ∈ s.pi t, Pi.cons s a y a_3 = b) → a_1 ≠ b
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : 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 = f x

Tactic:
Set.mulIndicator_of_mem h,

Goal state after:
case pos
α : 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
⊢ f x * sᶜ.mulIndicator g x = f x
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (⋯ ▸ fun x ↦ List.find? (fun b ↦ decide (p b)) l₁) = fun x ↦ List.find? (fun b ↦ decide (p b)) l₂

Tactic:
eqRec_eq_cast,

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (cast ⋯ fun x ↦ List.find? (fun b ↦ decide (p b)) l₁) = fun x ↦ List.find? (fun b ↦ decide (p b)) l₂
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| e

Tactic:
rw [← one_mul e, ← h, one_mul]

Goal state after:
R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| e * e
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ Set.InjOn f ↑(s.preimage f hf)

Tactic:
by simpa [mem_preimage, Set.InjOn] using hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
⊢ Nontrivial (α →₀ M)

Tactic:
inhabit α

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
inhabited_h : Inhabited α
⊢ Nontrivial (α →₀ M)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd✝ : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
f1✝ f2✝ : α →₀ M
hd : Disjoint f1✝.support f2✝.support
x : α
hx : x ∈ f1✝.support
⊢ g x (f1✝ x + f2✝ x) = g x (f1✝ x)

Tactic:
by
      simp only [notMem_support_iff.mp (disjoint_left.mp hd hx), add_zero]

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

Goal state before:
pp: α : Type u_1
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ s.sum f * b = s.sum fun a c ↦ f a c * b

Tactic:
simp only [Finsupp.sum, Finset.sum_mul]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ (map f s).prod < (map g s).prod

Tactic:
exact prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩

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

Goal state before:
pp: case c0
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ 0 ≤ ∏ i ∈ s, f i

pp: case b0
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ 0 ≤ g a

pp: case h₁
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ f a ≤ g a

pp: case h₂
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
b : β
h : ¬(mapDomain (⇑f) x) b = 0
⊢ ∃ a, ¬x a = 0 ∧ f a = b

Tactic:
obtain ⟨a, rfl⟩ := mem_range_of_mapDomain_ne_zero h
    exact ⟨a, by simpa [f.injective] using h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_12
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
⊢ equivMapDomain f l = mapDomain (⇑f) l

Tactic:
ext x; simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_9
inst✝² : AddCommGroup G
inst✝¹ : LinearOrder G
inst✝ : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Tactic:
by
  rw [abs_of_nonneg (Finset.sum_nonneg hf)]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})
⊢ ∑ b ∈ t, #({a ∈ s | f a = b}) = #s

Tactic:
← card_eq_sum_card_fiberwise Hf

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})
⊢ #s = #s
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
N : Type u_6
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : AddCommMonoid N
f : (i : ι) × αs i → M → N
⊢ l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun a b ↦ f ⟨i, a⟩ b

Tactic:
by
  simp only [sum, sigma_support, sum_sigma, split_apply]

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

Goal state before:
pp: case intro
N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Finite G
b : N
g : G
val✝ : Fintype G
⊢ g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

Tactic:
simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]

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

Goal state before:
pp: M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ_inv
inst✝ : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
k : κ
n : N
⊢ (lcongr e₁ e₂).symm (single k n) = single (e₁.symm k) (e₂.symm n)

Tactic:
apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective
  simp

Goal state after: