mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons
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 : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
⊢ C hd.prod

Tactic:
replace HL := HL.1

Goal state after:
case cons
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 : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ C hd.prod
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
ha : Irreducible x
⊢ ¬IsSquare x

Tactic:
isSquare_iff_exists_sq

Goal state after:
M : Type u_2
inst✝ : Monoid M
x : M
ha : Irreducible x
⊢ ¬∃ r, x = r ^ 2
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Tactic:
exact associated_mul_unit_left _ _ hu

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
⊢ IsRelPrime p n ↔ ¬p ∣ n

Tactic:
by
  refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩
  contrapose hpn
  suffices Associated p d from this.dvd.trans hdn
  exact (hp.dvd_iff.mp hdp).resolve_left hpn

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 ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
← closure_eq s,

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}
⊢ x ∈ closure ↑s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
⊢ map f ⊤ ≤ p ↔ comap f p = ⊤

Tactic:
map_le_iff_le_comap,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
⊢ ⊤ ≤ comap f p ↔ comap f p = ⊤
Module: Mathlib.Algebra.Module.Submodule.Range

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

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

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ map p.subtype p₁ ≤ map p.subtype p₂ ↔ p₁ ≤ p₂

Tactic:
map_le_iff_le_comap,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ p₁ ≤ comap p.subtype (map p.subtype p₂) ↔ p₁ ≤ p₂
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (insert 0 s) = span R s

Tactic:
refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))
  rw [span_le, Set.insert_subset_iff]
  exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩

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:
covBy_iff_Ioo_eq,

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

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

Tactic:
covBy_iff_Ioo_eq,

Goal state after:
α : 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) = ∅
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

Tactic:
refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)
  apply (OrderIso.to_galoisConnection (AddSubmonoid.toNatSubmodule (M := M)).symm).l_le
     (a := span ℕ s) (b := AddSubmonoid.closure s)
  rw [span_le]
  exact AddSubmonoid.subset_closure

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ↑(t ∪ u) ⊆ s

Tactic:
coe_union

Goal state after:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ↑t ∪ ↑u ⊆ s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
hs : s.Finite
⊢ (supClosure s).Finite

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ (supClosure ↑s).Finite
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
p p' : Submodule R M
P : M → Prop
⊢ (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

Tactic:
by
  simp [mem_sup]
  aesop

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
refine ⟨fun h => by simp [h], fun h => ?_⟩
  rw [le_antisymm_iff, le_iff_atom_le_imp, le_iff_atom_le_imp]
  simp_all

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
S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

Tactic:
by
  classical
  refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x - ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
this : Disjoint (f i) (f j) → Disjoint (f j) (({i, j}.erase j).sup f)
⊢ {i, j}.SupIndep f ↔ Disjoint (f i) (f j)

Tactic:
by
    simpa [supIndep_iff_disjoint_erase, hij]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
⊢ b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥} → (fun b ↦ ⨅ i, t i (b i)) b₁ = (fun b ↦ ⨅ i, t i (b i)) b₂ → b₁ = b₂

Tactic:
hb₂

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
⊢ (fun b ↦ ⨅ i, t i (b i)) b₁ = (fun b ↦ ⨅ i, t i (b i)) b₂ → b₁ = b₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas

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

Tactic:
isSquare_iff_exists_sq

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∃ r, ∏ i ∈ s, f i = r ^ 2
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at hc

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case cons
R : Type u_5
inst✝ : NonUnitalSemiring R
a x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ (x :: l).sum

Tactic:
rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

Goal state after:
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
a : List α
l : List (List α)
⊢ (↑a ::ₘ ↑(List.map (fun l ↦ ↑l) l)).Sections =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))

Tactic:
sections_cons,

Goal state after:
α : Type u_1
a : List α
l : List (List α)
⊢ ((↑a).bind fun a ↦ map (cons a) (↑(List.map (fun l ↦ ↑l) l)).Sections) =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))
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
⊢ p ⊔ q = map f (comap f p) ⊔ map f (comap f q)

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
⊢ p ⊔ q ≤ f.range

Tactic:
map_comap_eq_self hp,

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
⊢ p ⊔ q = p ⊔ map f (comap f q)

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
⊢ p ⊔ q ≤ f.range
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
⊢ map f ⊤ ≤ map f p ↔ Codisjoint p f.ker

Tactic:
map_le_iff_le_comap,

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 : Submodule R M
⊢ ⊤ ≤ comap f (map f p) ↔ Codisjoint p f.ker
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:
map_le_iff_le_comap,

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
⊢ p ⊓ (q ⊔ f.ker) ≤ comap f ⊥
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ Eq.ndrec (motive := fun x ↦ {x_1 | x_1 ∈ x ∧ p x_1}.Subsingleton → Option α)
      (fun x ↦ List.find? (fun b ↦ decide (p b)) l₁) ⋯ =
    fun x ↦ List.find? (fun b ↦ decide (p b)) l₂

Tactic:
unfold Eq.ndrec

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (⋯ ▸ fun x ↦ List.find? (fun b ↦ decide (p b)) l₁) = fun x ↦ List.find? (fun b ↦ decide (p b)) l₂
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₂
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ f.ker

Tactic:
map_le_iff_le_comap,

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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p p' : Submodule R M
⊢ p ≤ comap f (map f p') ↔ p ≤ p' ⊔ f.ker
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rw [← mem_range] at hnk
    rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
d : ι →₀ α
⊢ (d = indicator s fun i x ↦ d i) ↔ d.support ⊆ s

Tactic:
grind [indicator]

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

Goal state before:
pp: case pos
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∈ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

Tactic:
rcases h with ⟨a, rfl⟩
      simp

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
⊢ (f + g) x = (g + f) x

Tactic:
by_cases hg : x ∈ g.support

Goal state after:
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

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.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 = single a b + f

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

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

Goal state before:
pp: α : Type u_1
M : Type u_8
M' : Type u_9
N : Type u_10
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : x✝¹ ∉ (mapRange f hf g).support
⊢ h x✝¹ 0 = 1

Tactic:
h0

Goal state after:
α : Type u_1
M : Type u_8
M' : Type u_9
N : Type u_10
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : x✝¹ ∉ (mapRange f hf g).support
⊢ 1 = 1
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ?m.24

Tactic:
apply single_multiset_sum

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (f a✝).support ⊔ s✝.sup fun x ↦ (f x).support

Tactic:
exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
this : f i = ∏ j ∈ s, if i = j then f i else 1
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ 0 ≤ if i = x✝¹ then f i else 1

Tactic:
by grind [zero_le_one]

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

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 1 ≤ (map f s').prod

Tactic:
simp_all [one_le_prod]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_7
s : ι → Set α
x : α →₀ M
⊢ x ∈ supported M R (⋂ i, s i) ↔ x ∈ ⨅ i, supported M R (s i)

Tactic:
simp [mem_supported, subset_iInter_iff]

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : x ∉ Finite.toFinset hf
⊢ f x.down = 1

Tactic:
rwa [hf.mem_toFinset, notMem_mulSupport] at hxf

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ico i j = Ico ↑i ↑j

Tactic:
rw [← preimage_val_Ico_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans j.is_lt

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexFinsetRange.repr (b i)) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (single ⟨b i, ⋯⟩ 1) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ #{i | p i} ≤ ↑k

Tactic:
rw [← Fin.card_Iio]

Goal state after:
n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ #{i | p i} ≤ #(Iio k)
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : ℕ → α
⊢ (univ.sup fun n_1 ↦ f ↑n_1) = (range n).sup f

Tactic:
by
  rw [← image_fin_univ, sup_image, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → β → M
hs : s.Finite
ht : t.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:

Tactic:
f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
        Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
      _ = ∏ᶠ j, f j :=
        (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ a ≡ 0 [PMOD p] ↔ ∃ z, a = z • p

Tactic:
by
  rw [modEq_comm, modEq_iff_eq_add_zsmul]
  simp_rw [zero_add]

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

Goal state before:
pp: case neg
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : ¬Even n
⊢ 1 + (-1) ^ n = 0

Tactic:
· simp [(Nat.not_even_iff_odd.mp h).neg_pow]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ n.gcd (n - m) = 1 ↔ n.gcd m = 1

Tactic:
gcd_self_sub_right h

Goal state after:
m n : ℕ
h : m ≤ n
⊢ n.gcd m = 1 ↔ n.gcd m = 1