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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x y : R
⊢ (↑↑(algebraMap R A)).toFun (x • y) = (RingHom.id R) x • (↑↑(algebraMap R A)).toFun y

Tactic:
by simp [Algebra.smul_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ f = g

Tactic:
apply DFunLike.ext
  intro m
  exact DFunLike.congr_fun h m

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • y

Tactic:
intros; ext x; exact smul_add _ _ _

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₂ N₂
inst✝² : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ f x = default x

Tactic:
by rw [Subsingleton.elim x 0, map_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : M
inst✝¹ : IsCancelMulZero R
inst✝ : IsTorsionFree R M
hm : m ≠ 0
⊢ Function.Injective fun x ↦ x • m

Tactic:
by
  rintro r₁ r₂ hr
  dsimp at hr
  rwa [← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left hm, sub_eq_zero] at hr

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑s ∪ ↑t → c • x ∈ ↑s ∪ ↑t

Tactic:
by aesop

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑s ∩ ↑t → c • x ∈ ↑s ∩ ↑t

Tactic:
by aesop

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

Goal state before:
pp: S✝ : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋃ s ∈ S, ↑s → c • x ∈ ⋃ s ∈ S, ↑s

Tactic:
by aesop

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

Goal state before:
pp: S✝ : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋂ s ∈ S, ↑s → c • x ∈ ⋂ s ∈ S, ↑s

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬↑u + ↑u = 0

Tactic:
← two_mul,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬2 * ↑u = 0
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y z : R
hx : x ∈ s
hy : -y ∈ s
hz : z ∈ s
⊢ x * -y * z ∈ s

Tactic:
by aesop

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective fun n ↦ q ^ n

Tactic:
refine .of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
  · exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
  · exact (pow_mul_pow_sub q h.le).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ hd * tl.prod = -L.prod

Tactic:
hhd,

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ -1 * tl.prod = -L.prod
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x → IsUnit y ∨ x ~ᵤ y

pp: case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x

Tactic:
· rintro ⟨z, hz⟩
    obtain (h | h) := hx.isUnit_or_isUnit hz
    · exact Or.inl h
    · rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)

Goal state after:
case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ p * ↑u * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
rw [hu]

Goal state after:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ hd * tl.prod = L.prod

Tactic:
hhd,

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ -1 * tl.prod = L.prod
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
inst✝ : SMulCommClass R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ {r} • N
⊢ t • n ∈ N

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
by
    obtain ⟨a, ha⟩ := hs
    obtain ⟨b, hb⟩ := ht
    simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
    exact ⟨fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩, by simp_all⟩

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⋖ a ⊔ b → a ⊓ b ⋖ b

Tactic:
simp_rw [covBy_iff_Ioo_eq, sup_comm a, inf_comm a, ← isEmpty_coe_sort, right_lt_sup,
      inf_lt_left, (infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr]
    exact id

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)

Tactic:
· simp [prodMk_sup'_sup']

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ (s ×ˢ t).SupIndep f

Tactic:
Finset.product_eq_biUnion

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t).SupIndep f
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]
    grind [= SupIndep]

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hu : sSup s = u
h_le : k ≤ u
⊢ ∃ x ∈ s, k ≤ x

Tactic:
rw [← hu] at h_le

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hu : sSup s = u
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : 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 ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))

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

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
Sne : S.Nonempty
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = t.sup id
⊢ k ≤ t.sup id

Tactic:
rwa [← htsup]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ j ∉ t ∪ ↑s₀

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.SupIndep

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

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1

Tactic:
split_ifs with h_1

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : ¬x ∈ s
⊢ 1 = 1
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case right
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ k ≤ t.sup id

Tactic:
rwa [← htsup]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ ∏ j ∈ s, f j = 0

Tactic:
by
  classical rw [← prod_erase_mul _ _ hi, h, mul_zero]

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_1, (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) → ¬a = ⊥ ∧ a ∈ s

Tactic:
by aesop

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

Goal state before:
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
w✝¹ : x ∈ ⨆ i, p i
Cx : motive x w✝¹
w✝ : y ∈ ⨆ i, p i
Cy : motive y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx

Tactic:
exact ⟨_, add _ _ _ _ Cx Cy⟩

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'
xx : M
yy : M'
⊢ xx ∈ p ⊔ p' → yy ∈ q₁ ⊔ q₁' → (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
hxx

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'
xx : M
yy : M'
hxx : xx ∈ p ⊔ p'
⊢ yy ∈ q₁ ⊔ q₁' → (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
s t : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
hst : s ⊆ t
⊢ #s = ∑ i ∈ t, if i ∈ s then 1 else 0

Tactic:
by simp [hst]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Tactic:
classical
    simp_rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, ← h1, right_distrib]
    congr 2 <;> apply prod_congr rfl <;> simpa

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 : Submodule R M
⊢ comap f (map f p) = p ⊔ f.ker

Tactic:
by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))
  rintro x ⟨y, hy, e⟩
  exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩

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

Goal state before:
pp: case insert
ι : 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 ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) = ∏ x ∈ (insert a s).attach, f (↑x) (Pi.cons s a b g ↑x ⋯)

Tactic:
rw [attach_insert, prod_insert, prod_image]

Goal state after:
case insert
ι : 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 ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) =
    f (↑⟨a, ⋯⟩) (Pi.cons s a b g ↑⟨a, ⋯⟩ ⋯) * ∏ x ∈ s.attach, f (↑⟨↑x, ⋯⟩) (Pi.cons s a b g ↑⟨↑x, ⋯⟩ ⋯)

case insert
ι : 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 ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ Set.InjOn (fun x ↦ ⟨↑x, ⋯⟩) ↑s.attach

case insert
ι : 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 ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ ⟨a, ⋯⟩ ∉ image (fun x ↦ ⟨↑x, ⋯⟩) s.attach
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup (s ∪ {a}))

pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x ∧ x ≤ c

Tactic:
· rw [sSup_union, sSup_singleton]
    exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x ∧ x ≤ c
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
⊢ find? p s ⋯ = some (choose p s hp)

Tactic:
ext a
  refine find?_eq_some_iff _ |>.trans ?_
  simp only [Option.some.injEq, choose_eq_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ f.support = ∅ ↔ f = 0

Tactic:
exact support_eq_empty

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α → M
hf : (Function.support f).Finite
⊢ (ofSupportFinite f hf).support = hf.toFinset

Tactic:
by
  ext; simp [ofSupportFinite_coe]

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 [Int.ediv_mul_cancel (hf _ hs)]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (single i b).support (single j b').support ↔ i ≠ j

Tactic:
support_single _ hb,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint {i} (single j b').support ↔ i ≠ j
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
h : f a = 0
b : M
⊢ f.update a b = f + single a b

Tactic:
by
  rw [update_eq_erase_add_single, erase_of_notMem_support (by simpa)]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
mulIndicator_of_notMem hx

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ 1 = ⨆ i, (s i).mulIndicator f x