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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b

Tactic:
refine
        (hp.2.2 (f a) (f b) <| by
              convert! map_dvd f h
              simp).imp
          ?_ ?_ <;>
      · intro h
        convert! ← map_dvd g h <;> apply hinv

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

Goal state before:
pp: case inr
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 ∣ a

Tactic:
have : a ^ n.succ * x ^ n = p * y := by
    refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
    rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]

Goal state after:
case inr
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
this : a ^ n.succ * x ^ n = p * y
⊢ p ∣ a
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * ↑u * ↑u⁻¹ = x

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * (↑u * ↑u⁻¹) = x
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

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:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂

Tactic:
exact hp₁.dvd_of_dvd_pow this

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

Goal state before:
pp: case mp.mk
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ ∃ x, x * a = 0 ∧ x ≠ 0

Tactic:
refine ⟨x, ?_, ?_⟩

Goal state after:
case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x * a = 0

case mp.mk.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x ≠ 0
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
⊢ s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (map f s)

Tactic:
rw [← map_le_iff_le_comap, map_sup, f.map_closure]

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' ⇑f ⁻¹' {0}) ≤ map f s
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
hp : Prime p
n : ℕ
⊢ q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i

Tactic:
induction n generalizing q with
  | zero =>
    simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
  | succ n ih =>
    refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
    rw [pow_succ'] at h
    rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
    · rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
      rcases h with ⟨i, hi, hq⟩
      refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
      rw [pow_succ']
    · obtain ⟨i, hi, hq⟩ := ih.mp hno
      exact ⟨i, hi.trans n.le_succ, hq⟩

Goal state after:
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 S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
r : S
n : M
hr : r ∈ {a}
hn : n ∈ N
⊢ p' (r • n) ⋯

Tactic:
push _ ∈ _ at hr

Goal state after:
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 S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
r : S
n : M
hr✝ : r ∈ {a}
hn : n ∈ N
hr : r = a
⊢ p' (r • n) ⋯
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_4
G : Type u_5
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
S : Submodule R M
⊢ stabilizer G S = stabilizer G ↑S

Tactic:
by
  ext
  rw [mem_stabilizer_iff, SetLike.ext'_iff, coe_pointwise_smul,
    ← mem_stabilizer_iff]

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
h : 0 ∈ s
⊢ span R (s \ {0}) = span R s

pp: case neg
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
h : 0 ∉ s
⊢ span R (s \ {0}) = span R s

Tactic:
· rw [← span_insert_zero, show insert 0 (s \ {0}) = s by simp [h]]

Goal state after:
case neg
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
h : 0 ∉ s
⊢ span R (s \ {0}) = span R s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
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 a - _ ⟨y, hy, z, hz, rfl⟩

Goal state after:
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
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx✝ : y + z ∈ span R (↑p ∪ ↑p')
⊢ ∃ y_1 ∈ p, ∃ z_1 ∈ p', y_1 + z_1 = a • (y + z)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iic (e.symm.symm a) = Iic (e a)

Tactic:
e.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iic (e a) = Iic (e a)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iio (e.symm.symm a) = Iio (e a)

Tactic:
e.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iio (e a) = Iio (e a)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioo (e.symm.symm a) (e.symm.symm b) = Ioo (e a) (e b)

Tactic:
e.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioo (e a) (e b) = Ioo (e a) (e b)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioc (e.symm.symm a) (e.symm.symm b) = Ioc (e a) (e b)

Tactic:
e.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioc (e a) (e b) = Ioc (e a) (e b)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Icc (e.symm.symm a) (e.symm.symm b) = Icc (e a) (e b)

Tactic:
e.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Icc (e a) (e b) = Icc (e a) (e b)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyCoatomic α

Tactic:
rw [isAtomic_iff_isCoatomic] at h
  exact isStronglyCoatomic

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k → ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
intro hk

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
⊢ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
intro hk

Goal state after:
case mp
α : 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 α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Algebra.Module.Torsion.Field

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_2
inst✝² : DivisionSemiring 𝕜
inst✝¹ : AddCommMonoid M
inst✝ : Module 𝕜 M
r : 𝕜
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
simpa [hr.ne_zero] using congr(r⁻¹ • $hm)

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
intro hk

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
⊢ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
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)

pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
· simpa using h 2

Goal state after:
case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s ↦ ⨆ i ∈ s, f i
s t : Finset ι
⊢ ∃ z ∈ range g, (fun x1 x2 ↦ x1 ≤ x2) (g s) z ∧ (fun x1 x2 ↦ x1 ≤ x2) (g t) z

Tactic:
exact
        ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_right⟩

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (algebraMap S A) ((algebraMap R S) x) * (algebraMap S A) y * z = (algebraMap R A) x * ((algebraMap S A) y * z)

Tactic:
mul_assoc,

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (algebraMap S A) ((algebraMap R S) x) * ((algebraMap S A) y * z) = (algebraMap R A) x * ((algebraMap S A) y * z)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = ((algebraMap S A).comp (algebraMap R S)) x

Tactic:
simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
let S := { x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x }
  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩
  refine ⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩
  · classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
  · rw [Finset.sup_id_eq_sSup]
    exact sSup_le_sSup ht₁

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

Goal state before:
pp: case refine_4.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
x✝² : M
hx✝ : x✝² ∈ span R (⋃ i, ↑(p i))
r : R
x✝¹ : M
x✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
hx : x✝¹ ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)

Goal state after:
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
x✝² : M
hx✝ : x✝² ∈ span R (⋃ i, ↑(p i))
r : R
x✝¹ : M
x✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
hx : x✝¹ ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ ↑(p i)
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✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective ⇑f
hp : p ≤ f.range
hq : q ≤ f.range
⊢ comap f (p ⊔ q) = comap f p ⊔ comap f q

Tactic:
apply map_injective_of_injective hf

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective ⇑f
hp : p ≤ f.range
hq : q ≤ f.range
⊢ map f (comap f (p ⊔ q)) = map f (comap f p ⊔ comap f q)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : 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
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup ((s ∪ {x}) \ {x}))

Tactic:
simp only [Set.mem_singleton, Set.insert_sdiff_of_mem, Set.union_singleton]

Goal state after:
case inl
α : 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
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))
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₂
S : Submodule R M
hf : f.range = ⊤
⊢ (f.domRestrict S).range = ⊤ ↔ Codisjoint S f.ker

Tactic:
rw [← hf, LinearMap.range_domRestrict, map_eq_range_iff]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
⊢ a ^ #t * b ^ (#s - #t) = (∏ i ∈ t, a) * ∏ i ∈ s \ t, b

Tactic:
rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∈ f.support
hg : x ∈ g.support
⊢ (f + g) x = (g + f) x

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∈ f.support
hg : x ∉ g.support
⊢ (f + g) x = (g + f) x

Tactic:
· exact h _ (mem_inter_of_mem hf hg)

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∈ f.support
hg : x ∉ g.support
⊢ (f + g) x = (g + f) x
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
⊢ (erase a f) a = 0

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ (erase a f) a' = f a'

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ erase a (single a b) = 0

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ erase a (single a' b) = single a' b

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
⊢ erase a f = f

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ erase a f = f.update a 0

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a a' : α
ha : a ≠ a'
b : M
⊢ erase a (f.update a' b) = (erase a f).update a' b

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ erase a (erase a f) = erase a f

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ (erase a f).update a b = f.update a b

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ erase a (f.update a b) = erase a f

Tactic:
classical grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : M → N
hf : f 0 = 0
a : α
b : M
⊢ mapRange f hf (single a b) = single a (f b)

Tactic:
classical grind

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ ↑(-u) • x = -(u • x)

Tactic:
Units.val_neg,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -↑u • x = -(u • x)
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case ha
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ 0 ≤ f i

Tactic:
exact hf i hi

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y : M
⊢ (single x y).frange ⊆ {y}

Tactic:
classical grind

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

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

Tactic:
mul_assoc,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    ∑ x ∈ s, 2 * (r x * ((∑ i ∈ s, g i) * ∑ i ∈ s, r i))
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

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

Tactic:
mul_assoc,

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