mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
⊢ ∃ n, pred^[n] b = a

Tactic:
rcases eq_or_lt_of_le (pred_le b) with hb | hb

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b = b
⊢ ∃ n, pred^[n] b = a

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
⊢ ∃ n, pred^[n] b = a
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ b - (b - a) = a

Tactic:
tsub_tsub_cancel_of_le h

Goal state after:
m n a b : ℕ
h : a ≤ b
⊢ a = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a = succ ⊥ ∨ a ≤ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Tactic:
le_bot_iff,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a = succ ⊥ ∨ a = ⊥ ↔ a = ⊥ ∨ a = succ ⊥
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) ≤ f a) → Monotone f

Tactic:
simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ IsMin a

Tactic:
rw [← pred_eq_iff_isMin]

Goal state after:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ pred a = a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: n : ℕ
α : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = pure x

Tactic:
by
  rintro ⟨x, rfl⟩; dsimp [Vector.traverse, cast]
  induction x with | nil => rfl | cons x xs IH => simp! [IH]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ (∃ a', f a' = x ∧ r a' b) ↔ ∃ a', g a' = x ∧ r a' b

Tactic:
exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
right; exact le_trans hyz (le_map z)

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂

Tactic:
by
  induction hc₁ with
  | @succ c₃ hc₃ ih =>
    obtain ih | ih := ih
    · exact Or.inl (ih.trans subset_succChain)
    · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
  | union _ ih =>
    refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_
    exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_3
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f '' d✝ = Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })

pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
· simp [← hc, ← (Set.range_comp f ⇑c)]

Goal state after:
case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous fun x ↦ f x <*> g x

Tactic:
simp only [seq_eq_bind_map]
  exact ωScottContinuous.bind hf <| ωScottContinuous.of_apply₂ fun _ ↦ ωScottContinuous.map hg

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

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

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

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

Goal state before:
pp: α : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
classical
  simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoidWithOne R
⊢ ∀ (n : ℕ), op ↑(n + 1) = op ↑n + 1

Tactic:
simp [add_comm]

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

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

Tactic:
simp [add_comm]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ (↑↑(φ₁.comp ↑φ₂)).toFun ((algebraMap R A) r) = (algebraMap R C) r

Tactic:
rw [← φ₁.commutes, ← φ₂.commutes]

Goal state after:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ (↑↑(φ₁.comp ↑φ₂)).toFun ((algebraMap R A) r) = φ₁ (φ₂ ((algebraMap R A) r))
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x

Tactic:
induction hx using AddSubgroup.closure_induction with
  | mem _ hx =>
    obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx
    exact ⟨[l], by simp_all⟩
  | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
  | add _ _ _ _ hL hM =>
    obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
    exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
      rw [List.map_append, List.sum_append, HL2, HM2]⟩
  | neg _ _ hL =>
    obtain ⟨L, hL⟩ := hL
    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.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ ↑u * y = ↑u * (A * B)

Tactic:
← HAB

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ ↑u * y = ↑u * y
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ y * ↑u = A * B * ↑u

Tactic:
← HAB

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ y * ↑u = y * ↑u
Module: Mathlib.Algebra.GroupWithZero.Associated

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

Tactic:
by
  simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]
  constructor <;> intro h b c dvd <;> obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd
  · obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm
    exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
  · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩

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

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
x : M
hx : f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z ∈ p

Tactic:
suffices z + x - x ∈ p by simpa only [this, add_sub_cancel_right]

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
x : M
hx : f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z + x - x ∈ p
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z = x✝ ⊔ y ⊓ z

Tactic:
rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ z ⊓ y ⊔ x✝ = z ⊓ (y ⊔ x✝)
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ y ≤ x

Tactic:
rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
⊢ y ≤ x
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)

Tactic:
closure_union_closure_right,

Goal state after:
α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑(l.toFun ↑x) ∪ ↑y) = l.toFun (↑x ∪ ↑y)
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ SupClosed (insert a s)

Tactic:
SupClosed

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ SupClosed (insert a s)

Tactic:
SupClosed

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ x = -a • y + (x + a • y)

Tactic:
simp [add_comm]

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

Goal state before:
pp: R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute x y
⊢ ∀ y ∈ span R s, Commute x y

Tactic:
simp only [Commute.symm_iff (a := x)] at *

Goal state after:
R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
⊢ ∀ y ∈ span R s, Commute y x
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]
    exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩

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

Goal state before:
pp: case mpr.mem
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x : M
hx : x ∈ S
⊢ f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩

Tactic:
exact h ⟨x, hx⟩

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

Goal state before:
pp: case 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))
x : M
hx : x ∈ ⋃ i, ↑(p i)
⊢ x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
exact AddSubmonoid.subset_closure hx

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
⊢ sSupIndep (⋃ i, s i)

Tactic:
rintro a ⟨_, ⟨i, _⟩, _⟩

Goal state after:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i ↦ s i) i = w✝
⊢ Disjoint a (sSup ((⋃ i, s i) \ {a}))
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x✝¹ : (i : ι) → M i
x✝ : ι
⊢ ∏ c, mulSingle c (x✝¹ c) x✝ = x✝¹ x✝

Tactic:
exact Fintype.prod_pi_mulSingle ..

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ iSupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
rw [iSupIndep_iff_supIndep]
  intro s
  induction s using Finset.strongInduction with
  | H s ih =>
    by_cases hs : 1 < s.card; swap
    · by_cases hcard0 : s.card = 0 <;> grind [Finset.card_eq_zero, Finset.card_eq_one]
    · obtain ⟨k₁, k₂, _, _, h⟩ := Finset.one_lt_card_iff.mp hs
      obtain ⟨i, hi⟩ : ∃ i : ι, k₁ i ≠ k₂ i := Function.ne_iff.mp h
      classical
      rw [← Finset.image_biUnion_filter_eq s (· i)]
      refine Finset.SupIndep.biUnion ?_ (by grind)
      apply ((h_indep i).supIndep' _).mono
      simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
      rintro _ _ _ _ rfl
      exact iInf_le _ _

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
⊢ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i) = ⊤

Tactic:
refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b : α
h : sSup {a | a ≤ b ∧ IsAtom a} = b
s : Set α
s_ind : sSupIndep s
left✝ : Disjoint ⊥ (sSup s)
s_atoms : ⊥ ⊔ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
⊢ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
by simpa using s_atoms

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : IsEmpty α
f g : α →₀ M
⊢ f = g

Tactic:
by ext x; exact isEmptyElim x

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support = {a ∈ s | f a ≠ 0}

Tactic:
dsimp [onFinset]; rw [onFinsetSupport]; congr

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

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

Tactic:
refine f.induction zero ?_
  convert! add_single using 7
  apply (addCommute_of_disjoint _).eq
  simp_all

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ single none 0 = 0

Tactic:
single_zero

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ 0 = 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • f x

Tactic:
rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, HasFiniteMulSupport (f i)
hs : s.Nonempty
⊢ HasFiniteMulSupport fun a ↦ s.sup' hs fun x ↦ f x a

Tactic:
by
  simp only [HasFiniteMulSupport] at hf ⊢
  refine (s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_
  simp only [mem_mulSupport, SetLike.mem_coe, Set.mem_iUnion, exists_prop] at ha ⊢
  contrapose! ha
  exact Finset.sup'_eq_of_forall hs (fun x ↦ f x a) ha

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : i ∉ (indicator s f).support
⊢ single i 0 = 0

Tactic:
single_zero

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : i ∉ (indicator s f).support
⊢ 0 = 0
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 1 ≤ a
⊢ 1 ≤ s.prod

Tactic:
cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
  apply List.one_le_prod h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α ≃ β
l : α →₀ M
g : β → M → N
⊢ (equivMapDomain f l).prod g = l.prod fun a m ↦ g (f a) m

Tactic:
simp [prod, equivMapDomain]

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ (single (f a) 0) (f a) = 0

Tactic:
rw [single_zero, coe_zero, Pi.zero_apply]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s, ¬i_1 = i → 0 ≤ f i_1

Tactic:
exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

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 : α →₀ M
g : β →₀ M
⊢ mapDomain Sum.swap (f.sumElim g) = g.sumElim f

Tactic:
simp [sumElim_eq_add, mapDomain_add, ← mapDomain_comp, Function.comp_def, add_comm]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ succ '' Iic i = Ioc 0 i.succ

Tactic:
refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_le_succ_iff.2 hj⟩) ?_

Goal state after:
n : ℕ
i : Fin n
⊢ Ioc 0 i.succ ⊆ succ '' Iic i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁷ : Fintype α
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : SMulCommClass R S M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ ((Fintype.bilinearCombination R S) v) (Pi.single i r) = r • v i

Tactic:
simp [Fintype.bilinearCombination]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) (repr R w x) = ↑x

Tactic:
rw [Span.repr_def]
  exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : p 0
⊢ #{x | p x.succ} + 1 = 1 + #{x | p x.succ}

Tactic:
simp [add_comm]

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : ¬p 0
⊢ #{x | p x.succ} = 0 + #{x | p x.succ}

Tactic:
simp [add_comm]

Goal state after: