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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
h : t ≤ f.rangeS
⊢ map f (comap f t) = t

Tactic:
by
  simpa only [inf_of_le_left h] using map_comap_eq f t

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a b : M
inst✝ : Subsingleton Mˣ
hab : Irreducible (a * b)
⊢ a = 1 ∨ b = 1

Tactic:
simpa using hab.isUnit_or_isUnit rfl

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

Goal state before:
pp: 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
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | one => exact one_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | neg _ _ h => exact neg_left _ _ _ _ h
  | zero => exact zero_right x hx
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | neg _ _ h => exact neg_right _ _ _ _ h

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

Goal state before:
pp: case neg
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✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x✝

Tactic:
exact ⟨L.map (List.cons (-1)),
      List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
      hL.2 ▸
        List.recOn L (by simp)
          (by simp +contextual [List.map_cons, add_comm])⟩

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
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ~ᵤ d

Tactic:
exact (hp.dvd_iff.mp hdp).resolve_left hpn

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Quot.out (Associates.mk a) ~ᵤ a

Tactic:
rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ b = a * ⟨c, ⋯⟩

Tactic:
Subtype.ext_iff,

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ ↑b = ↑(a * ⟨c, ⋯⟩)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

Tactic:
IsRelPrime,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∀ ⦃d : Associates M⦄, d ∣ Associates.mk a → d ∣ Associates.mk b → IsUnit d) ↔ ∀ ⦃d : M⦄, d ∣ a → d ∣ b → IsUnit d
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
⊢ map f (s ⊔ closure (⇑f ⁻¹' {0})) ≤ map f s

Tactic:
map_sup,

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 ⊔ map f (closure (⇑f ⁻¹' {0})) ≤ map f s
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk (a * 0) = Associates.mk 0

Tactic:
mul_zero

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk 0 = Associates.mk 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
⊢ ∀ {a : Associates M}, a ≠ 0 → IsLeftRegular a

Tactic:
by
      rintro ⟨a⟩ ha ⟨b⟩ ⟨c⟩ h
      rcases Quotient.exact' h with ⟨u, hu⟩
      have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
      exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
⊢ p ≤ ⊥ ↔ p = ⊥

Tactic:
le_bot_iff

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
⊢ p = ⊥ ↔ p = ⊥
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₂
⊢ f.range = ⊥ ↔ f.range ≤ ⊥

Tactic:
le_bot_iff

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₂
⊢ f.range = ⊥ ↔ f.range = ⊥
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
x : P
hx : x ∈ (f ∘ₗ g - id).ker
⊢ f (g x) = x

Tactic:
simpa [sub_eq_zero] using hx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁)) x✝¹)) x✝ = ((algebraMap R (Module.End S M₂)) x✝¹) x✝

Tactic:
change e.restrictScalars R _ = _

Goal state after:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (restrictScalars R e) (((algebraMap R (Module.End S M₁)) x✝¹) (↑e.symm x✝)) =
    ((algebraMap R (Module.End S M₂)) x✝¹) x✝
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ (N₁ ⊔ N₂).submoduleOf N = N₁.submoduleOf N ⊔ N₂.submoduleOf N

Tactic:
apply Submodule.map_injective_of_injective N.subtype_injective
  simp only [submoduleOf, map_comap_eq]
  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
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
have key {v} : v ∈ span R s ↔ v ∈ closure (@univ R • s) := by simp [← span_eq_closure]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ p x hx
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
⊢ ∃ b, x ⊓ ↑b = a ∧ Codisjoint x ↑b

Tactic:
obtain ⟨y, rfl, hcodisjoint⟩ := exists_inf_eq_and_codisjoint hx

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x y : α
hcodisjoint : Codisjoint x y
x✝ : ↑(Ici (x ⊓ y))
hx : x ∈ Ici (x ⊓ y)
⊢ ∃ b, x ⊓ ↑b = x ⊓ y ∧ Codisjoint x ↑b
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
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + (y₂ + z₂))

Tactic:
← add_assoc z₁,

Goal state after:
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')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + 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 : α
⊢ ⇑e '' Iic a = Iic (e a)

Tactic:
e.image_eq_preimage_symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e.symm ⁻¹' Iic 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 : α
⊢ ⇑e '' Iio a = Iio (e a)

Tactic:
e.image_eq_preimage_symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e.symm ⁻¹' Iio 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 : α
⊢ ⇑e '' Ioo a b = Ioo (e a) (e b)

Tactic:
e.image_eq_preimage_symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e.symm ⁻¹' Ioo a 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 : α
⊢ ⇑e '' Ioc a b = Ioc (e a) (e b)

Tactic:
e.image_eq_preimage_symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e.symm ⁻¹' Ioc a 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 : α
⊢ ⇑e '' Icc a b = Icc (e a) (e b)

Tactic:
e.image_eq_preimage_symm,

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

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a : α
hab : a < a
ha'b : ⊥ ≤ a
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ ∃ x, a ⋖ x ∧ x ≤ a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f

Tactic:
Finset.supIndep_iff_disjoint_erase

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
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 ≠ ⊥
⊢ i ∈ s

Tactic:
by_contra contra
  replace h₁ : Disjoint (f i) (⨆ i ∈ s, f i) := (h₁ i).mono_right <| biSup_mono <| by aesop
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
⊢ (g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x

Tactic:
by
  rw [← mulIndicator_comp_right, preimage_image_eq _ hg]

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
⊢ (∏ x ∈ s.erase i, f x) * 0 = 0

Tactic:
mul_zero

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ 0 = 0
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ a ≤ b

Tactic:
rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ sSup {c | IsCompactElement c ∧ c ≤ a} ≤ sSup {c | IsCompactElement c ∧ c ≤ b}
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
intro c

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
⊢ IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
intro c

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
⊢ IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
h : (insert i (t.preimage f hf)).SupIndep f
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))

Tactic:
Finset.supIndep_iff_disjoint_erase

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
h : ∀ i_1 ∈ insert i (t.preimage f hf), Disjoint (f i_1) (((insert i (t.preimage f hf)).erase i_1).sup f)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
⊢ Set.EqOn (fun b ↦ ∏ i ∈ v, f i b) (fun b ↦ ∏ i ∈ v, f' i b) s

Tactic:
convert! eqOn_finsetProd h v

Goal state after:
case e'_3
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f i x✝ = (∏ i ∈ v, f i) x✝

case e'_4
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f' i x✝ = (∏ i ∈ v, f' i) 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✝⁵ : 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)

Tactic:
map_sup,

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) ⊔ map f (comap f q)
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:
simp_rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, ← h1, right_distrib]

Goal state after:
ι : 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
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]

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
⊢ ⟨a, ⋯⟩ ∉ image (fun x ↦ ⟨↑x, ⋯⟩) s.attach

Tactic:
simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

Goal state after:
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:
by
    unfold Eq.ndrec
    rw [eqRec_eq_cast, cast_eq_iff_heq]
    refine Function.hfunext ?_ (fun hp₁ hp₂ _ ↦ heq_of_eq ?_)
    · congr!
      exact congrArg _ (Quotient.sound h)
    refine List.find?_eq_find?_of_perm h ?_
    simpa using hp₁

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:
ext; simp [ofSupportFinite_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ l₁ a = l₂ a

Tactic:
by simpa only [embDomain_apply_self] using DFunLike.ext_iff.1 h (f a)

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 : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = ∑ t ∈ s.powerset, (∏ i ∈ t, a) * ∏ i ∈ s \ t, b

Tactic:
refine Finset.sum_congr rfl fun t ht => ?_

Goal state after:
ι : 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
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
by
  classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ (erase a f).support = s

Tactic:
rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ motive f

Tactic:
suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
  refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
  · rwa [support_eq_empty.1 h]
  · have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
    rw [← single_add_erase a f]
    refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
    rw [← mem_support_iff, hs]
    exact mem_insert_self a s

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
this : (optionElim y f) (Option.some a) = 0 (Option.some a)
⊢ f a = 0 a

Tactic:
simp only [optionElim_apply_eq_elim, Option.elim_some, coe_zero, Pi.zero_apply] at this

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
this : f a = 0
⊢ f a = 0 a
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : ¬x✝ ∈ s
⊢ 0 = 0 * 0

Tactic:
mul_zero

Goal state after:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : ¬x✝ ∈ s
⊢ 0 = 0