mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α ⊕ β)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩

Goal state after:
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α ⊕ β)
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α × β)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩

Goal state after:
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α × β)
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Sigma π)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩

Goal state after:
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
⊢ Countable (Sigma π)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ (ofFn f).tail.get i = f i.succ

Tactic:
get_tail,

Goal state after:
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ (ofFn f).get ⟨↑i + 1, ⋯⟩ = f i.succ
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
induction n generalizing b with
  | zero =>
    have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]
  | succ n hn =>
    rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp
    · intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (filter (fun x ↦ a ≠ x) ↑m).card + ↑⟨count a ↑m, ⋯⟩ = (↑m).card

Tactic:
rw [← countP_eq_card_filter, add_comm]
          simp only [eq_comm, Ne, count]
          rw [← card_eq_countP_add_countP _ _]

Goal state after:
Module: Mathlib.Logic.UnivLE

Goal state before:
pp: ⊢ ¬UnivLE.{u + 1, u}

Tactic:
simp only [univLE_iff, small_iff, not_forall, not_exists]
  exact ⟨Type u, fun α => fun ⟨f⟩ => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Tactic:
by
  refine (List.prod_set' v.toList i a).trans ?_
  simp [get_eq_get_toList, mul_assoc]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl a✝ = inl c✝

Tactic:
antisymm hab hba

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl c✝ = inl c✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr b✝ = inr d✝

Tactic:
antisymm hab hba

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr d✝ = inr d✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₁✝ = inl a₂✝

Tactic:
antisymm hab hba

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₂✝ = inl a₂✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₁✝ = inr b₂✝

Tactic:
antisymm hab hba

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₂✝ = inr b₂✝
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u
c : ι → Cardinal.{v}
⊢ lift.{w, max v u} (prod c) = prod fun i ↦ lift.{w, v} (c i)

Tactic:
by
  lift c to ι → Type v using fun _ => trivial
  simp only [← mk_pi, ← mk_uLift]
  exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
h : s b (f a)
⊢ ∃ a', f a' = b ∧ r a' a

Tactic:
by
    rcases f.mem_range_of_rel h with ⟨a', rfl⟩
    exact ⟨a', rfl, f.map_rel_iff.1 h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑f '' s)

Tactic:
by
  change IsUpperSet ((f : α ≃ β) '' s)
  rw [Equiv.image_eq_preimage_symm]
  exact hs.preimage f.symm.monotone

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.snd

Tactic:
by
  intro d hd₁ hd₂ hd₃ a ha
  simp only [isLUB_prod] at ha
  exact ha.2

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := pd, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := pd, get := p }

Tactic:
by
    have t : od = pd := propext H1
    cases t; rw [show o = p from funext fun p => H2 p p]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ a ∈ (f.bind g).bind k ↔ a ∈ f.bind fun x ↦ (g x).bind k

Tactic:
simp only [mem_bind_iff]
    exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
⊢ r y z ∨ r z y

Tactic:
rcases hcs₁ hsy hsz hsseq with h | h

Goal state after:
case refine_1.inr.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sy ⊆ sz
⊢ r y z ∨ r z y

case refine_1.inr.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sz ⊆ sy
⊢ r y z ∨ r z y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ h; congr

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toNat #α = toNat #β

Tactic:
by
  -- Porting note: Inserted universe hint below
  rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ (∃ b, a = ↑b) ↔ a ≤ ℵ₀

Tactic:
simpa only [mem_range, eq_comm] using! Set.ext_iff.1 range_ofENat a

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
P✝ : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N✝
inst✝³ : Monoid P✝
N : Type u_4
P : Type u_5
inst✝² : Monoid N
inst✝¹ : Monoid P
φ : N →* N
inst✝ : IsId φ
ψ : N →* P
⊢ ψ.comp φ = ψ

Tactic:
by simp only [IsId.eq_id, MonoidHom.comp_id]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ 1 < #α ↔ Nontrivial α

Tactic:
← not_le,

Goal state after:
α : Type u
⊢ ¬#α ≤ 1 ↔ Nontrivial α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ ℵ₀ < #α ↔ Uncountable α

Tactic:
← not_le,

Goal state after:
α : Type u
⊢ ¬#α ≤ ℵ₀ ↔ Uncountable α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
· exact Or.inl hb

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ #↑univ = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
mk_set_eq_nat_iff_finset

Goal state after:
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ t, ↑t = univ ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
⊢ #↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

Tactic:
refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩
  apply card_le_of (fun s ↦ ?_)
  classical
  let u : Finset α := s.image Subtype.val
  have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
  grind

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 S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ✝ : R →+* S
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
this : σ = RingHom.id R
⊢ r • x = σ r • x

Tactic:
subst this

Goal state after:
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 S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
r : R
x : M
inst✝ : RingHomId (RingHom.id R)
⊢ r • x = (RingHom.id R) r • x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
x m : ↥p
⊢ x ∈ MulAction.orbit R m ↔ ↑x ∈ MulAction.orbit R ↑m

Tactic:
by
  rw [← val_preimage_orbit, Set.mem_preimage]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Submonoid.map f (algebraMapSubmonoid A M) = algebraMapSubmonoid B M

Tactic:
ext x
  constructor
  · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
    simp only [AlgHom.commutes]
    use r
  · rintro ⟨r, hr, rfl⟩
    simp only [Submonoid.mem_map]
    use (algebraMap R A r)
    simp only [AlgHom.commutes, and_true]
    use r

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure (insert (↑n) s) = closure s

Tactic:
by
  rw [Set.insert_eq, closure_union]
  simp

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure (insert (↑n) s) = closure s

Tactic:
by
  rw [Set.insert_eq, closure_union]
  simp

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
exact (pow_mul_pow_sub q h.le).symm

Goal state after:
Module: Mathlib.Order.ModularLattice

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

Tactic:
rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ i, f i
ha' : ¬∃ i, a ≤ f i
⊢ False

Tactic:
push Not at ha'

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
⊢ False
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 : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(f r) = x

Tactic:
eq

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = x
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a ⊓ b, isSublattice_latticeClosure.infClosed ha hb, map_inf ..⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t

Tactic:
simp_rw [← supClosure_infClosure]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)
Module: Mathlib.Order.Atoms

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

Tactic:
by
  rw [← isAtomic_iff_isCoatomic] at h
  exact isStronglyAtomic

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b

Tactic:
apply (lt_or_eq_of_le hle).resolve_left _

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
⊢ ¬sSup {a | IsAtom a ∧ a ≤ b} < b
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ ∃ y ∈ s, ∃ z, (z ∈ t ∧ z ∈ p) ∧ y + z = x

Tactic:
refine ⟨y, hy, z, ⟨hz, ?_⟩, hyzx⟩

Goal state after:
case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ z ∈ p
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : 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 ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ a✝ a ⋯ = b✝ a ⋯

Tactic:
eq

Goal state after:
ι : 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 ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ b✝ a ⋯ = b✝ a ⋯
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
α : 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 ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_sdiff_of_notMem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa
      rw [h, sSup_union, sSup_singleton]
      apply
        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
          (a_dis_Sup_s.mono_right _).symm
      rw [← sSup_insert, Set.insert_sdiff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ≠ 0
⊢ Disjoint s (K ∙ x) ↔ x ∉ s

Tactic:
by
  simp [disjoint_span_singleton, hx]

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
⊢ Disjoint s (K ∙ x)

Tactic:
by
  simp [disjoint_span_singleton, hx]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α → M
⊢ {a}.indicator f = ⇑(single a (f a))

Tactic:
Set.indicator_singleton,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α → M
⊢ Pi.single a (f a) = ⇑(single a (f a))
Module: Mathlib.Data.Finsupp.Single

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

Tactic:
eq

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ (single a b₂) a = (single a b₂) a
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ single a b = single a' b' ↔ b = b'

Tactic:
by
  rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]

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
i : α
inst✝ : DecidableEq α
⊢ (f.update a b) i = if i = a then b else f i

Tactic:
delta update Function.update
  grind

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ((equivFunOnFinite.symm f).sum fun x n ↦ n) = ∑ a, f a

Tactic:
by
  rw [equivFunOnFinite_symm_eq_sum, sum_fintype _ _ fun _ ↦ rfl, coe_univ_sum_single]

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

Goal state before:
pp: case b0
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ g a

Tactic:
· apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
a : α
h : ¬(mapDomain (⇑f) x) (f a) = 0
⊢ ¬x a = 0 ∧ f a = f a

Tactic:
simpa [f.injective] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (s : Multiset α), (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod

Tactic:
refine Multiset.induction (by simp [h_one]) ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod) →
      (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (mapDomain f s).prod h = s.prod fun a b ↦ h (f a) b

Tactic:
← Function.Embedding.coeFn_mk f hf,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (mapDomain (⇑{ toFun := f, inj' := hf }) s).prod h = s.prod fun a b ↦ h ({ toFun := f, inj' := hf } a) b
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
⊢ mapDomain f v₁ = mapDomain f v₂ → v₁ = v₂

Tactic:
eq

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂