mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn • (a + a') = mn • a + mn • a'

Tactic:
change mn.1 • mn.2 • _ = (_ : α)

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • mn.2 • (a + a') = mn • a + mn • a'
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝² : SetLike S M
inst✝¹ : SMul R M
inst✝ : SMulMemClass S R M
r : R
s : S
x : M
hx : x ∈ ↑s
⊢ (fun x ↦ r • x) x ∈ ↑s

Tactic:
simpa using SMulMemClass.smul_mem (r : R) hx

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n : ℤ
x✝ : M
⊢ ↑n * x✝ = x✝ * ↑n

Tactic:
Int.commute_cast

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n : ℤ
x✝ : M
⊢ ↑n * x✝ = ↑n * x✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ (a * x✝¹ + b * x✝¹) * x✝ = (a + b) * x✝¹ * x✝

Tactic:
← add_mul

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ (a + b) * x✝¹ * x✝ = (a + b) * x✝¹ * x✝
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case add
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (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 ⋯
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
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonUnitalNonAssocRing 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 ⋯
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
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure ↑M

Tactic:
refine Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ fun _ hx ↦ ?_)

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ ↑M ⊆ ↑M.subsemiringClosure.toNonUnitalSubsemiring

case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case add
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
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case add
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
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ ∀ (head : List R) (tail : List (List R)),
    (List.map List.prod (List.map (List.cons (-1)) tail)).sum = -(List.map List.prod tail).sum →
      (List.map List.prod (List.map (List.cons (-1)) (head :: tail))).sum = -(List.map List.prod (head :: tail)).sum

Tactic:
by simp +contextual [List.map_cons, add_comm]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * p ^ n * x ^ n

Tactic:
mul_comm _ (p ^ n),

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * a ^ n.succ * x ^ n
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x ~ᵤ y ↔ x = y

Tactic:
by
  simp [Associated, Units.eq_one]

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ closure (↑s ∪ ⇑f ⁻¹' {0})

Tactic:
← add_sub_cancel y x

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : ¬s ⊆ 0 ∧ ¬t = 0
hst : (s * t).Nonempty
⊢ False

Tactic:
← hst.of_smul_right.subset_zero_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
hst : (s * t).Nonempty
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
⊢ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s ⊔ t → n ∈ N → r • n ∈ s • N ⊔ t • N

Tactic:
rintro _ _ (hr | hr) hn
        · exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)
        · exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc (a ⊓ b) a)
⊢ ↑((fun x ↦ ⟨a ⊓ ↑x, ⋯⟩) ((fun x ↦ ⟨↑x ⊔ b, ⋯⟩) x)) = ↑x

Tactic:
by
        change a ⊓ (↑x ⊔ b) = ↑x
        rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a < b ⊔ a ∧ Ioo a (b ⊔ a) = ∅ → b ⊓ a < b ∧ Ioo (b ⊓ a) b = ∅

Tactic:
← isEmpty_coe_sort,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a < b ⊔ a ∧ IsEmpty ↑(Ioo a (b ⊔ a)) → b ⊓ a < b ∧ IsEmpty ↑(Ioo (b ⊓ a) b)
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⊓ b < a ∧ Ioo (a ⊓ b) a = ∅ → b < a ⊔ b ∧ Ioo b (a ⊔ b) = ∅

Tactic:
← isEmpty_coe_sort,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⊓ b < a ∧ IsEmpty ↑(Ioo (a ⊓ b) a) → b < a ⊔ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)

Tactic:
rw [closure_union_closure_right, closure_union_closure_left]

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
x✝ y✝ : N
hx✝ : x✝ ∈ span R t
hy✝ : y✝ ∈ span R t
h₁ : p a x✝ ha hx✝
h₂ : p a y✝ ha hy✝
⊢ p a (x✝ + y✝) ha ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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 ∉ K, x ∈ H ∧ H ≠ L)

Tactic:
← and_assoc,

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 ≤ K ∧ H ≠ L ↔ ∃ x, (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
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 ∉ H, x ∈ L ∧ H ≠ K)

Tactic:
← and_assoc,

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, (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : 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
⊢ f '' latticeClosure s = latticeClosure (f '' s)

Tactic:
simp only [subset_antisymm_iff, Set.image_subset_iff]

Goal state after:
α : 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
⊢ latticeClosure s ⊆ f ⁻¹' latticeClosure (f '' s) ∧ latticeClosure (f '' s) ⊆ f '' latticeClosure s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j + r • v i))) = span R (range v)

Tactic:
by
  refine le_antisymm ?_ ?_ <;> simp only [span_le, Set.range_subset_iff, SetLike.mem_coe] <;>
    intro k <;> obtain rfl | hjk := eq_or_ne j k
  · rw [update_self]
    exact add_mem (subset_span ⟨j, rfl⟩) <| smul_mem _ _ <| subset_span ⟨i, rfl⟩
  · exact subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩
  · nth_rw 2 [← add_sub_cancel_right (v j) (r • v i)]
    exact sub_mem (subset_span ⟨j, update_self ..⟩)
      (smul_mem _ _ (subset_span ⟨i, update_of_ne hij ..⟩))
  · exact subset_span ⟨k, update_of_ne hjk.symm ..⟩

Goal state after:
Module: Mathlib.Order.SupIndep

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

Tactic:
induction s using Finset.induction_on generalizing t with

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = (∏ x, ⋯.choose) * ∏ x, ⋯.choose

Tactic:
← Finset.prod_mul_distrib,

Goal state after:
case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = ∏ x, ⋯.choose * ⋯.choose
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
s : Finset ι
f : ι → κ → M₀
x : κ
⊢ (x ∈ support fun j ↦ ∏ i ∈ s, f i j) ↔ x ∈ ⋂ i ∈ s, support (f i)

Tactic:
by simp [support, prod_eq_zero_iff]

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

Goal state before:
pp: case mpr
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:
· intro h
    simp [h]

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

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

Tactic:
· intro h
    simp [h]

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
⊢ ∏ x, (φ x) (mulSingle i m x) = (φ i) m

Tactic:
let φ' i : M i → M' := ⇑(φ 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)
⊢ ∏ x, (φ x) (mulSingle i m x) = (φ i) m
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
ι : 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)
val✝ : Fintype ι
⊢ p f

Tactic:
← Finset.univ_prod_mulSingle f

Goal state after:
case intro
ι : 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)
val✝ : Fintype ι
⊢ p (∏ i, Pi.mulSingle i (f i))
Module: Mathlib.LinearAlgebra.Span.Basic

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
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, p i
i : ι
x : M
hx : x ∈ p i
⊢ ∃ (hx : x ∈ ⨆ i, p i), motive x hx

pp: case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ ∃ (hx : 0 ∈ ⨆ i, p i), motive 0 hx

pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, p i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, p i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx

Tactic:
· exact ⟨_, mem _ _ hx⟩

Goal state after:
case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ ∃ (hx : 0 ∈ ⨆ i, p i), motive 0 hx

case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, p i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, p i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map ((fun x ↦ Prod.map id (cons a) x) ∘ fun t ↦ (s - t, t)) s.powerset +
      map ((fun x ↦ Prod.map (cons a) id x) ∘ fun t ↦ (s - t, t)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map ((fun x ↦ (a ::ₘ s - x, x)) ∘ cons a) s.powerset

Tactic:
Function.comp,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ Prod.map id (cons a) (s - x, x)) s.powerset + map (fun x ↦ Prod.map (cons a) id (s - x, x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (a ::ₘ s - a ::ₘ x, a ::ₘ x)) s.powerset
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₂
hf : Surjective ⇑f
p : Submodule R M
le : f.ker ≤ p
hp : IsCoatom p
⊢ IsCoatom (comap f (map f p))

Tactic:
comap_map_eq_self le

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₂
hf : Surjective ⇑f
p : Submodule R M
le : f.ker ≤ p
hp : IsCoatom p
⊢ IsCoatom p
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₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
h : p ⋖ q
⊢ comap f p ⋖ comap f q

Tactic:
refine ⟨lt_of_le_of_ne (comap_mono h.1.le) ((comap_injective_of_surjective hf).ne h.1.ne), ?_⟩

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₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
h : p ⋖ q
⊢ ∀ ⦃c : Submodule R M⦄, comap f p < c → ¬c < comap f q
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α ↔ IsAtomistic α

Tactic:
constructor <;> intros

Goal state after:
case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α

case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ (a : α), a ∈ onFinsetSupport s f ↔ f a ≠ 0

Tactic:
by simpa [onFinsetSupport]

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

Goal state before:
pp: case inr
ι : Type u_5
s✝ : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n > 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Tactic:
rw [Nat.div_mul_cancel (hf _ hs)]

Goal state after: