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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

Tactic:
obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
lt : s b ↑(collapseF f m)
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

case h.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a m : α
h : s (↑(collapseF f m)) ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}, ¬r x m
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = ↑(collapseF f m)

case h.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
gt : s (↑(collapseF f m)) b
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
⊢ IsMin (f a) ↔ IsMin a

Tactic:
refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩
  obtain ⟨x, rfl⟩ := f.mem_range_of_le hb
  rw [f.le_iff_le] at hb ⊢
  exact h hb

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o

Tactic:
dsimp [restrict, mem_eq]; constructor
  · rintro ⟨h₀, h₁⟩
    exact ⟨h₀, ⟨_, h₁⟩⟩
  rintro ⟨h₀, _, h₂⟩; exact ⟨h₀, h₂⟩

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

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s✝ ∨ ⋃₀ s✝ ⊆ c₂

Tactic:
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.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:
induction hc₁ with

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂

Tactic:
induction hc₁ with

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

Goal state before:
pp: case inl
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : IsEmpty β
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
have : IsEmpty α := Function.isEmpty f
    exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective, by simp⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ (f (ωSup c)) (g (ωSup c)) = ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
· rw [hf.map_ωSup, hg.map_ωSup]
    simp only [ωSup_def, ωSup_apply]
    apply le_antisymm
    · apply ωSup_le
      intro i
      dsimp
      rw [(f (c i)).continuous]
      apply ωSup_le
      intro j
      apply le_ωSup_of_le (i ⊔ j)
      apply apply_mono
      · apply hf.monotone (c.monotone le_sup_left)
      · apply hg.monotone (c.monotone le_sup_right)
    · simp only [ωSup_le_iff]
      intro i
      apply le_ωSup_of_le i
      apply (f (c i)).monotone
      apply le_ωSup_of_le i
      rfl

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
a b : ULift.{u, v} (Quotient.out (f i))
h : (fun a ↦ ⟨i, a.down⟩) a = (fun a ↦ ⟨i, a.down⟩) b
⊢ a = b

Tactic:
by simpa using h

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

Goal state before:
pp: x y : Cardinal.{u}
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
by
    wlog hle : x ≤ y; · rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]
    cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_mul, toENatAux_nat]
    | inr hy =>
      rcases eq_or_ne x 0 with rfl | hx
      · simp
      · simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

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

Goal state before:
pp: c : Cardinal.{u}
x✝ : c ≤ ℵ₀ ∨ ℵ₀ ≤ c
⊢ toENat (lift.{v, u} c) = toENat c

Tactic:
cases le_total c ℵ₀ with

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

Goal state before:
pp: case coe
m : ℕ
hm : ↑m ≠ 0
⊢ ↑↑m * ℵ₀ = ℵ₀

Tactic:
rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: N : Type u_1
P : Type u_2
φ : N → N
inst✝ : IsId φ
ψ : N → P
⊢ ψ ∘ φ = ψ

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

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.univ.card

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ

Tactic:
by simpa using h

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

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
⊢ Sum.elim 0 (f + g) = Sum.elim 0 f + Sum.elim 0 g

Tactic:
ext (i | i)

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim 0 (f + g) (inl i) = (Sum.elim 0 f + Sum.elim 0 g) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim 0 (f + g) (inr i) = (Sum.elim 0 f + Sum.elim 0 g) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
⊢ Sum.elim 0 (t • f) = (RingHom.id R) t • Sum.elim 0 f

Tactic:
ext (i | i)

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : κ
⊢ Sum.elim 0 (t • f) (inl i) = ((RingHom.id R) t • Sum.elim 0 f) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : ι
⊢ Sum.elim 0 (t • f) (inr i) = ((RingHom.id R) t • Sum.elim 0 f) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
⊢ Sum.elim (f + g) 0 = Sum.elim f 0 + Sum.elim g 0

Tactic:
ext (i | i)

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim (f + g) 0 (inl i) = (Sum.elim f 0 + Sum.elim g 0) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim (f + g) 0 (inr i) = (Sum.elim f 0 + Sum.elim g 0) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
⊢ Sum.elim (t • f) 0 = (RingHom.id R) t • Sum.elim f 0

Tactic:
ext (i | i)

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : ι
⊢ Sum.elim (t • f) 0 (inl i) = ((RingHom.id R) t • Sum.elim f 0) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : κ
⊢ Sum.elim (t • f) 0 (inr i) = ((RingHom.id R) t • Sum.elim f 0) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup N₁
inst✝² : Module R M
inst✝¹ : Module R N₁
inst✝ : Nontrivial M
m : M
ne : m ≠ 0
⊢ Nontrivial (End R M)

Tactic:
exact nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p

Tactic:
by
  rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p q : SubMulAction R M
h : p.carrier = q.carrier
⊢ p = q

Tactic:
by cases p; cases q; congr

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ + b✝ ∈ {0}

Tactic:
by simp_all

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ * b✝ ∈ {0}

Tactic:
by simp_all

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
f : A →ₗ[R] B
map_one : f 1 = 1
map_mul : ∀ (x y : A), f (x * y) = f x * f y
c : R
⊢ f ((algebraMap R A) c) = (algebraMap R B) c

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, f.map_smul, map_one]

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

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

Tactic:
by simp_all

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

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0 ∨ y = 0
⊢ y = 0

Tactic:
by simp_all

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
this : n = 1
⊢ Prime p ∧ n = 1

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
r : S
n : M
hr : r ∈ {a}
hn : n ∈ N
⊢ p' (r • n) ⋯

Tactic:
· push _ ∈ _ at hr
    subst hr
    exact smul₀ n hn

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
by simp_all

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 b (a ⊔ b))
⊢ ↑((fun c ↦ ⟨↑c ⊔ b, ⋯⟩) ((fun c ↦ ⟨a ⊓ ↑c, ⋯⟩) c)) = ↑c

Tactic:
by
      dsimp
      rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : Frame α
s : Set α
a : α
ha : IsAtom a
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

Tactic:
by
  simp [sSup_eq_iSup', ha.le_iSup]

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
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ R ∙ m ≤ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
le_iSup_iff

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
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
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
T : Finset M
hTs : ↑T ⊆ s
htT : ↑t ⊆ ↑(span R ↑T)
T' : Finset M
hT's : ↑T' ⊆ s
haT' : a ∈ span R ↑T'
⊢ ↑(T ∪ T') ⊆ s

Tactic:
by simp_all

Goal state after:
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
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
AddSubgroup.mem_sup

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
n : ℕ
hn : a n = sSup (range ⇑a)
m : ℕ
hm : n ≤ m
⊢ ¬sSup (range ⇑a) < a m

Tactic:
exact (le_sSup (mem_range_self m)).not_gt

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ ∀ (i : ↑s), sSupIndep ↑i

Tactic:
by simpa using h

Goal state after:
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'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
⊢ Finset.univ.prod (mulSingle i (φ' i m)) = (φ i) m

Tactic:
show φ' i = φ i from rfl

Goal state after:
ι✝ : 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'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
⊢ Finset.univ.prod (mulSingle i ((φ i) m)) = (φ i) m
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ (a ::ₘ s).antidiagonal = map (fun t ↦ (a ::ₘ s - t, t)) (a ::ₘ s).powerset

Tactic:
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
      id, sub_cons, erase_cons_head]
    rw [add_comm]
    congr 1
    refine Multiset.map_congr rfl fun x hx ↦ ?_
    rw [cons_sub_of_le _ (mem_powerset.mp hx)]

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

Goal state before:
pp: case neg.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
con : ⟨c, ⋯⟩ = ⊥
⊢ c ∈ {⊥}

Tactic:
simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con

Goal state after:
case neg.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
con : c = ⊥
⊢ c ∈ {⊥}
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
b : R
h : ∀ i ∈ s, Commute b (f i)
i : ι
hi : i ∈ s.val
hb : f i ∈ Multiset.map (fun i ↦ f i) s.val
⊢ Commute b (f i)

Tactic:
exact h _ hi

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

Goal state before:
pp: R✝¹ : Type u_1
R₂ : Type u_2
K : Type u_3
M✝¹ : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
R✝ : Type u_8
M✝ : Type u_9
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u_10
M : Type u_11
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : Submodule R M
hxy : x✝⁴ ≤ x✝²
x✝¹ : M
x✝ : x✝¹ ∈ (x✝⁴ ⊔ x✝³) ⊓ x✝²
⊢ x✝¹ ∈ x✝⁴ ⊔ x✝³ ⊓ x✝²

Tactic:
by rwa [← sup_inf_assoc_of_le_of_neg_le _ hxy (by simpa)]

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ sSup {a | a ≤ ⊤ ∧ IsAtom a} = ⊤

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∀ (a : α), (if a ∈ g.support then f a else 0) ≠ 0 → a ∈ g.support

Tactic:
by simp_all

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

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

Tactic:
(single_injective a₂).eq_iff

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : b₁ = b₂
h : a₁ = a₂
⊢ b₁ = b₂
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂}

Tactic:
rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]
  · simp
  · simp [support_single, *]

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
a : Option α
⊢ a.elim y ⇑f = Option.elim' y (⇑f) a

Tactic:
Option.elim'_eq_elim

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a : Option α
⊢ a.elim y ⇑f = a.elim y ⇑f
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x, Pi.single x m i = m

Tactic:
Finset.sum_pi_single

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ f s.prod ≤ (map f s).prod

Tactic:
by
  induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_of_submultiplicative f h_one h_mul]

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

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map (fun i ↦ max (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
Multiset.quot_mk_to_coe'',

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (map f ↑l).prod (map g ↑l).prod ≤ (map (fun i ↦ max (f i) (g i)) ↑l).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i ↦ min (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    min (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
Multiset.quot_mk_to_coe'',

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i ↦ min (f i) (g i)) ↑l).prod ≤ min (map f ↑l).prod (map g ↑l).prod