mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ p ≤ comap f ⊥ ↔ map f p = ⊥

Tactic:
eq_bot_iff,

Goal state after:
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₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ p ≤ comap f ⊥ ↔ map f p ≤ ⊥
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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
⊢ comap f q < p

Tactic:
rw [← map_lt_map_iff_of_injective hf]

Goal state after:
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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
⊢ map f (comap f q) < map f p
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul.add_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ (x✝ + y✝) * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [add_mul] using add_mem h₁ h₂

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

Goal state before:
pp: case one
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
⊢ p x 1 hx ⋯

Tactic:
exact one_right x hx

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
⊢ (t ++ u).prod = x * y

Tactic:
by rw [List.prod_append, ht2, hu2]

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

Goal state before:
pp: case one
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
⊢ p x 1 hx ⋯

Tactic:
exact one_right x hx

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

Goal state before:
pp: case mul.add_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ (x✝ + y✝) * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa [add_mul] using add_mem h₁ h₂

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
x✝ : M₀
hx : x✝ ∈ S
⊢ x✝ ≠ 0

Tactic:
rintro rfl; exact hS hx

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

Goal state before:
pp: case inl
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Subsingleton M₀
⊢ Submonoid.map f S ≤ M₀'⁰

pp: case inr
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Nontrivial M₀
⊢ Submonoid.map f S ≤ M₀'⁰

Tactic:
· simp [Subsingleton.elim S ⊥]

Goal state after:
case inr
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Nontrivial M₀
⊢ Submonoid.map f S ≤ M₀'⁰
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = c * ↑v * d

Tactic:
mul_assoc c (v : M) d,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = c * (↑v * d)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
⊢ DecompositionMonoid (Associates M) ↔ DecompositionMonoid M

Tactic:
by
  simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r

Tactic:
obtain ⟨u, rfl⟩ := h'

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : DvdNotUnit p q
u : Mˣ
⊢ DvdNotUnit p (q * ↑u)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ q * ↑u = p * (x * ↑u)

Tactic:
rw [← mul_assoc, ← hx.right]

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

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

Tactic:
inv_mul_cancel

Goal state after:
R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑1 x = x
Module: Mathlib.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, Disjoint x ↑b ∧ x ⊔ ↑b = a

Tactic:
obtain ⟨y, hdisjoint, rfl⟩ := exists_disjoint_and_sup_eq hx

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x y : α
hdisjoint : Disjoint x y
x✝ : ↑(Iic (x ⊔ y))
hx : x ∈ Iic (x ⊔ y)
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = x ⊔ y
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 ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
⊢ (∃ a, ∃ z_1 ∈ span R {y, z}, w = a • x + z_1) ↔ ∃ a b c, a • x + b • y + c • z = w

Tactic:
simp_rw [mem_span_pair]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
refine ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ IsCoatom ⟨b, xb⟩
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
simpa using h 2

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → s.sup f ≤ sSup d → ∃ x ∈ d, s.sup f ≤ x

Tactic:
hemp

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → s.sup f ≤ sSup d → ∃ x ∈ d, s.sup f ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∀ x ∈ Finset.image f s, ∃ y ∈ d, x ≤ y

Tactic:
rintro x hx

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
⊢ ∃ y ∈ d, x ≤ y
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✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
⊢ restrictScalars R (span A X) = span R X

Tactic:
refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm
  refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm
  obtain ⟨r, rfl⟩ := hsur a
  simpa [algebraMap_smul] using smul_mem _ r hm

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

Goal state before:
pp: 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
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
b : R
c : S
x✝ : c ∈ span R s
hc : c • x ∈ span R (s • t)
⊢ b • c • x ∈ span R (s • t)

Tactic:
exact smul_mem _ _ hc

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a

Tactic:
simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]

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

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
j : ι
| (φ j) (mulSingle i m j)

Tactic:
rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
j : ι
| mulSingle i (φ' i m) j
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
x✝ : DecidableEq α
⊢ ∃ a, a ≤ x.1 + x.2 ∧ (a, x.1 + x.2 - a) = x

Tactic:
obtain ⟨x₁, x₂⟩ := x

Goal state after:
α : Type u_1
s : Multiset α
l : List α
x✝ : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ ∃ a, a ≤ (x₁, x₂).1 + (x₁, x₂).2 ∧ (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)
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
x : M
d : Set (Submodule R M)
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → R ∙ x ≤ sSup d → ∃ x_1 ∈ d, R ∙ x ≤ x_1

Tactic:
hemp

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → R ∙ x ≤ sSup d → ∃ x_1 ∈ d, R ∙ x ≤ x_1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = -span R s

Tactic:
by
  apply le_antisymm
  · rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
    exact subset_span
  · rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
    exact subset_span

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₂
p q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ map f (p ⊓ (q ⊔ f.ker)) = ⊥

Tactic:
eq_bot_iff,

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 q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ map f (p ⊓ (q ⊔ f.ker)) ≤ ⊥
Module: Mathlib.Data.List.Find

Goal state before:
pp: case trans
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton → find? p l₁✝ = find? p l₂✝
ih2 : {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton → find? p l₂✝ = find? p l₃✝
hp : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton
⊢ find? p l₁✝ = find? p l₃✝

Tactic:
refine (ih1 ?_).trans (ih2 ?_)

Goal state after:
case trans.refine_1
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton → find? p l₁✝ = find? p l₂✝
ih2 : {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton → find? p l₂✝ = find? p l₃✝
hp : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton
⊢ {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton

case trans.refine_2
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton → find? p l₁✝ = find? p l₂✝
ih2 : {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton → find? p l₂✝ = find? p l₃✝
hp : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton
⊢ {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ HasFiniteSupport ⇑f

Tactic:
rw [HasFiniteSupport]

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ (Function.support ⇑f).Finite
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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p'

Tactic:
rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
⊢ indicator {a} f = single a (f a ⋯)

Tactic:
ext j
  simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ f1.prod g1 = f2.prod g2

Tactic:
Finsupp.prod_of_support_subset f1 Finset.subset_union_left _ h1,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ ∏ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = f2.prod g2
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = (∏ x ∈ f.support ∪ g.support, h x (f x)) * g.prod h

Tactic:
Finsupp.prod_of_support_subset g subset_union_right h h_zero,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = (∏ x ∈ f.support ∪ g.support, h x (f x)) * ∏ x ∈ f.support ∪ g.support, h x (g x)
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f (-((↑n)⁻¹ • x)) = -((↑n)⁻¹ • f x)

Tactic:
map_neg,

Goal state after:
case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ -f ((↑n)⁻¹ • x) = -((↑n)⁻¹ • f x)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ (indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

Tactic:
rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
  refine Finset.prod_congr rfl (fun _ _ => ?_)
  rw [indicator_of_mem]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
· simp [hs0]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod