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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ succ (Classical.choose ⋯) ⋯ ≍ succ b hb

Tactic:
congr!

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ Classical.choose ⋯ = b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
⊢ isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a ≤ b ↔ a < b

Tactic:
succ_le_iff_of_not_isMax ha

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ a < b ↔ a < b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b

Tactic:
obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
hab : a < succ^[n] a
⊢ f a < f (succ^[n] a)
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise f (update g i v)

Tactic:
refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl

Goal state after:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
j : ι
hj : j ∈ s
⊢ j ≠ i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
· convert! (s.prod_inter_mul_prod_sdiff { i } f).symm
    simp [hs]

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
rw [Subtype.ext_iff, val_replicate, Multiset.eq_replicate]
  exact and_iff_right s.2

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
⊢ Countable (List α)

Tactic:
have := Encodable.ofCountable α
  infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i, f ↑i = ∏ i ∈ range n, f i

Tactic:
← attach_eq_univ,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i ∈ (range n).attach, f ↑i = ∏ i ∈ range n, f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Tactic:
unfold SymOptionSuccEquiv.encode
    split_ifs with h
    · obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h
      exact Option.some_ne_none _ ha
    · refine congr_arg Sum.inr ?_
      refine map_injective (Option.some_injective _) _ ?_
      refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_) <;> simp

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
⊢ ¬univ.Countable ↔ Uncountable α

Tactic:
rw [countable_univ_iff, not_countable_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ b, a < b

Tactic:
by
        obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)
        · exact (not_inr_lt_inl h).elim
        · exact ⟨b, inr_lt_inr_iff.1 h⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccLimit (sSup s)
⊢ sSup s ∈ s

Tactic:
rw [isSuccLimit_iff, not_and_or, not_not] at hlim
  rcases hlim with (hmin | hlim)
  · have ⟨a, has⟩ := hne
    rwa [← hmin.eq_of_le <| le_csSup hbdd has]
  · have ⟨y, hy⟩ := not_forall_not.mp hlim
    have ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
    exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ c ≤ a, f c = b) → b ≤ f a

Tactic:
· rintro ⟨c, hc, rfl⟩
    exact f.monotone hc

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
simp_rw [h.toOption, h.bind]

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun a ↦ (f a).toOption
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : ℕ → α
hf : Monotone f
⊢ ∀ ⦃a₂ : Chain α⦄,
    (fun c ↦ ⇑c.toOrderHom) { toFun := f, monotone' := hf } = (fun c ↦ ⇑c.toOrderHom) a₂ →
      { toFun := f, monotone' := hf } = a₂

Tactic:
congr!

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f = ⨆ n, (⇑f)^[n] ⊥

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥

case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f
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 α
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ })))) =
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
apply le_antisymm

Goal state after:
case a
α : 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 α
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ })))) ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

case a
α : 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 α
⊢ ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) = ωSup (iterateChain (↑f) x h)

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)

case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
simp only [lt_aleph0, mk_eq_nat_iff, finite_iff_exists_equiv_fin]

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

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

Tactic:
exact Or.inl ha

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑1 ≤ ↑n

Tactic:
Nat.cast_le,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ n
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r
⊢ P = Q

Tactic:
by
  replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h
  have h' : (haveI := P; (· • ·) : R → A → A) = (haveI := Q; (· • ·) : R → A → A) := by
    funext r a
    rw [P.smul_def', Q.smul_def', h]
  rcases P with @⟨⟨P⟩⟩
  congr

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

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ σ x • f 1 = g (x • 1)

Tactic:
g.map_smulₑ,

Goal state after:
R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ σ x • f 1 = σ x • g 1
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Monoid R
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulDistribMulAction R M
inst✝ : MulDistribMulAction R N
x✝² : R
x✝¹ x✝ : M × N
⊢ (x✝² • (x✝¹ * x✝)).1 = (x✝² • x✝¹ * x✝² • x✝).1

Tactic:
exact smul_mul' ..

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Monoid R
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulDistribMulAction R M
inst✝ : MulDistribMulAction R N
x✝² : R
x✝¹ x✝ : M × N
⊢ (x✝² • (x✝¹ * x✝)).2 = (x✝² • x✝¹ * x✝² • x✝).2

Tactic:
exact smul_mul' ..

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Nontrivial ↥p ↔ p ≠ ⊥

Tactic:
by
  rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

Tactic:
AddSubsemigroup.mem_carrier,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).toAddSubsemigroup
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).toAddSubsemigroup
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
x✝ t : NonUnitalSubsemiring R
s : AddSubmonoid R
hs : ∀ {a b : R}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
⊢ { toAddSubmonoid := s, mul_mem' := hs }.toAddSubmonoid = t.toAddSubmonoid →
    { toAddSubmonoid := s, mul_mem' := hs } = t

Tactic:
congr!

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n : ℕ
⊢ ↑n ∈ s

Tactic:
by
  induction n <;> simp [zero_mem, add_mem, one_mem, *]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
x✝ t : Subring R
s : Subsemiring R
hs : ∀ {x : R}, x ∈ s.carrier → -x ∈ s.carrier
⊢ { toSubsemiring := s, neg_mem' := hs }.toSubsemiring = t.toSubsemiring → { toSubsemiring := s, neg_mem' := hs } = t

Tactic:
congr!

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ∣ a * c

Tactic:
rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ comap f (map f s) = s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})

case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (map f s)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ comap f (map f s) = s

Tactic:
by
  convert! comap_map_eq f s
  rwa [left_eq_sup, closure_le]

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

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

Tactic:
eq_top_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₂
p : Submodule R₂ M₂
⊢ ⊤ ≤ comap f p ↔ ⊤ ≤ comap f p
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e ϕ : A₁ ≃ₐ[R] A₂
ψ χ : A₁ ≃ₐ[R] A₁
⊢ ϕ.symm.trans ((ψ * χ).trans ϕ) = ϕ.symm.trans (ψ.trans ϕ) * ϕ.symm.trans (χ.trans ϕ)

Tactic:
ext
    simp only [mul_apply, trans_apply, symm_apply_apply]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
⊢ IsLUB (supClosure s) a ↔ IsLUB s a

Tactic:
by simp [IsLUB]

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
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
⊢ p = sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := ⋯
⊢ p ≤ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := ⋯
⊢ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ⨆ a, ↑a ∈ s

Tactic:
exact hs.iSup_mem_of_nonempty (by simpa)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
hcon : ¬∃ x, a ⋖ x ∧ x ≤ b
x : α
hx : x ∈ s
⊢ x ≤ a

Tactic:
not_exists,

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ∀ (x : α), ¬(a ⋖ x ∧ x ≤ b)
⊢ x ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
by
    obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩
    obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'
    · obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint
      exact False.elim <| hab.ne rfl
    refine ⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩
    convert! hd.1.bot_covBy
    rw [← le_bot_iff, ← show a ⊓ a' = ⊥ by simpa using Subtype.coe_inj.2 ha'.inf_eq_bot, inf_comm]
    exact inf_le_inf_left _ hd.2

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
rw [isAtomic_iff_isCoatomic] at h

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyCoatomic α
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ (s ×ˢ t).SupIndep f

Tactic:
classical
  rw [Finset.product_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using! hs
  · exact fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s ↦ ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (range g)
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
have h2 : k ≤ sSup (Set.range g) :=
      h.trans
        (iSup_le fun i =>
          le_sSup_of_le ⟨{i}, rfl⟩
            (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s ↦ ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
⊢ SupClosed s → sSup s ∈ s

Tactic:
hsc

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
⊢ sSup s ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s = t.sup id

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s ≤ t.sup id

case a
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ t.sup id ≤ sSup s
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
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) = span R s

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) ≤ span R s

case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)
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₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : x ∈ span R s
⊢ f x ∈ map f (span R s)

Tactic:
exact Submodule.mem_map_of_mem h

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_8
inst✝² : Monoid α
inst✝¹ : DistribMulAction α M
inst✝ : SMulCommClass α R M
s : Set α
t : Set M
⊢ s • span R t = span R (s • t)

Tactic:
set_smul_eq_iSup,

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α : Type u_8
inst✝² : Monoid α
inst✝¹ : DistribMulAction α M
inst✝ : SMulCommClass α R M
s : Set α
t : Set M
⊢ ⨆ a ∈ s, a • span R t = span R (s • t)
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case nil
R : Type u_5
inst✝ : NonUnitalSemiring R
a : R
h : ∀ (x : R), x ∈ [] → a ∣ x
⊢ a ∣ [].sum

Tactic:
exact dvd_zero _

Goal state after: