mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case inl
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : c * z' = c * w'
⊢ z = w

Tactic:
← (f.map_units x).mul_left_inj,

Goal state after:
case inl
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : c * z' = c * w'
⊢ z * f ↑x = w * f ↑x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
⊢ n₁ = n₂

Tactic:
have ⟨ms₁, eq₁⟩ := f.surj n₁

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
⊢ n₁ = n₂
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
⊢ False

Tactic:
obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
    exact ha.not_ge (hm' a)

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
H : ¬IsMax a
⊢ False

Tactic:
exact h a (covBy_succ_of_not_isMax H)

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
⊢ ¬IsMin a

Tactic:
obtain rfl | hb := (hs.1 hb).eq_or_lt

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s : Set α
b : α
hb : b ∈ s
hs : IsLUB s b
ha : b ∉ s
⊢ ¬IsMin b

case inr
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb✝ : b ∈ s
hb : b < a
⊢ ¬IsMin a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
⊢ a < succ b → a ≤ b

Tactic:
by
  contrapose!
  exact succ_le_of_lt

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : F α✝
⊢ f✝ <$> x✝ = f✝ <$> x✝

Tactic:
exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)

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

Goal state before:
pp: α : Type u_1
n' : ℕ
s s' : Sym α n'
⊢ s.append s' = (Sym.cast ⋯) (s'.append s)

Tactic:
simp [append, add_comm]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : LT α
f : α ≤i β
h : f a ≤ f a
⊢ f a ∈ Set.range ⇑f

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LT α
f : α ≤i β
h : b ≤ f a
hb : b < f a
⊢ b ∈ Set.range ⇑f

Tactic:
exacts [⟨a, rfl⟩, f.mem_range_of_rel hb]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2

Tactic:
isLUB_le_iff (hg hd₁ hd₂ hd₃ hda),

Goal state after:
case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).2 ∈ upperBounds (g '' d)
Module: Mathlib.Data.Part

Goal state before:
pp: α : 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
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
by
  by_cases h : o.Dom
  · simp_rw [h.toOption, h.bind]
    rfl
  · rw [Part.toOption_eq_none_iff.2 h]
    exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

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

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

Tactic:
obtain ih | ih := ih

Goal state after:
case succ.inl
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast {y | IsExtremePt x f y} x

Tactic:
constructor
    · refine ⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩
      intro y hy hyx
      exfalso
      exact lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)
    · exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
⊢ y ∈ bot x f ↔ IsExtremePt x f y

Tactic:
by
  rw [← setOfPred_isExtremePt_eq_bot le_map, mem_ofPred]

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

Goal state before:
pp: α✝ β✝ : Type u
a b : Cardinal.{u}
α β : Type u
⊢ #α * #β = 0 → #α = 0 ∨ #β = 0

Tactic:
by
      simpa only [mul_def, mk_eq_zero_iff, isEmpty_prod] using id

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

Goal state before:
pp: α : 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, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
classical
  rcases isEmpty_or_nonempty β with hβ | hβ
  · have : IsEmpty α := Function.isEmpty f
    exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective, by simp⟩
  set F : Set α →o Set α :=
    { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
      monotone' := fun s t hst => by dsimp at hst ⊢; gcongr }
  set s : Set α := F.lfp
  have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
  have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
  set g' := invFun g
  have g'g : LeftInverse g' g := leftInverse_invFun hg
  have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
  set h : α → β := s.piecewise f g'
  have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
  have : Injective h := by
    refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
    · intro x hx y hy hxy
      obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
      obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _, g'g _] at hxy
      rw [hxy]
    · intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩
  refine ⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩
  simp only [h, Set.piecewise, g']
  split
  · exact hp₁ a
  · have : g (invFun g a) = a := by
      have : a ∈ g '' (f '' s)ᶜ := by grind
      obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this
      exact Function.invFun_eq ⟨x, hx⟩
    grind

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ (iterateChain (↑f) x h) 0 ≤ a

Tactic:
exact h_x_le_a

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

Goal state before:
pp: c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ∀ (a : ℕ), ↑a ≤ d
⊢ toNat c = toNat d

Tactic:
← Cardinal.aleph0_le

Goal state after:
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
⊢ toNat c = toNat d
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : ((fun m ↦ a • m) ∘ fun x ↦ s • x) c = ((fun m ↦ a • m) ∘ fun x ↦ s • x) d
⊢ c = d

Tactic:
dsimp only [Function.comp_def] at cd
  rw [← smul_assoc, ← smul_assoc] at cd
  exact ab cd

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 1 < b
⊢ a < b ^ a

Tactic:
by
  rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb
  exact (cantor a).trans_le (power_le_power_right hb)

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ∀ (n : ℕ), ↑n ≤ c
hn : c < ℵ₀
⊢ False

Tactic:
rcases lt_aleph0.1 hn with ⟨n, rfl⟩
    exact (Nat.lt_succ_self _).not_ge (Nat.cast_le.1 (h (n + 1)))

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

Goal state before:
pp: α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ lift.{v, u} #↑(⇑f ⁻¹' s) = lift.{u, v} #↑s

Tactic:
apply mk_preimage_of_injective_of_subset_range_lift _ _ f.injective
  rw [f.range_eq_univ]
  exact fun _ _ ↦ ⟨⟩

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
cases subsingleton_or_nontrivial α
    · exact Subsingleton.elim ..
    · exact unop_injective <| mul_left_cancel₀ one_ne_zero (h 1)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
n m : ℕ
h : ↑n = ↑m
x : M
hx : x ≠ 0
⊢ ↑n • x = ↑m • x

Tactic:
simp [← Nat.cast_smul_eq_nsmul R, h]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
c : S
fₗ : N →ₗ[S] N₂
h : fₗ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ c • fₗ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
dsimp at h
    exact le_trans h (comap_le_comap_smul qₗ fₗ c)

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

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = -x✝ * a

Tactic:
← ha.comm,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = a * -x✝
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: case h
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
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M ∧ f ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
simp only [AlgHom.commutes, and_true]

Goal state after:
case h
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
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
let U : Subsemiring R :=
    Subsemiring.mk' (⋃ i, (S i : Set R))
      (⨆ i, (S i).toSubmonoid) (Submonoid.coe_iSup_of_directed hS)
      (⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.coe_iSup_of_directed hS)

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q r : M
h : DvdNotUnit p r
h' : p ~ᵤ q
⊢ DvdNotUnit q r

Tactic:
obtain ⟨u, rfl⟩ := h'.symm
  obtain ⟨hp, x, hx⟩ := h
  have hq : q ≠ 0 := by simp_all
  refine ⟨hq, x * u, mt isUnit_of_mul_isUnit_left hx.1, ?_⟩
  rw [mul_comm x, ← mul_assoc, ← hx.2]

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₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : f ∘ₛₗ 0 = 0
⊢ f.ker.subtype.range = ⊥

Tactic:
← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)

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₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : f ∘ₛₗ 0 = 0
⊢ range 0 = ⊥
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
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ iSup S ↔ ∃ i, x ∈ S i

Tactic:
by
  rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]
  rfl

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inr.hnc
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
con : ⊥ ∈ s
⊢ False

Tactic:
exact top_ne_bot (eq_bot_iff.2 (h con))

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ IsLUB {f | IsAtom f ∧ f ≤ s} s

Tactic:
isLUB_pi

Goal state after:
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∀ (a : ι), IsLUB (Function.eval a '' {f | IsAtom f ∧ f ≤ s}) (s a)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
by
  let S := { x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x }
  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩
  refine ⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩
  · classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
  · rw [Finset.sup_id_eq_sSup]
    exact sSup_le_sSup ht₁

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
⊢ s.Finite

Tactic:
by_contra! contra
    obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
    replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
      have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.sdiff (Finset.finite_toSet _)
      obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
      exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
    obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
    replace hs : x ⊓ sSup s = ⊥ := by
      have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
      simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
    apply hx₁
    rw [← hs, eq_comm, inf_eq_left]
    exact le_sSup hx₀

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

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ∀ b ∈ s, b i = i_1 → ⨅ i, f i (b i) ≤ f i i_1

Tactic:
rintro _ _ _ _ rfl

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
b✝ : (i : ι) → κ i
a✝¹ : b✝ ∈ s
a✝ : b✝ i ∈ Finset.image (fun x ↦ x i) s
⊢ ⨅ i, f i (b✝ i) ≤ f i (b✝ i)
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
intro eq

Goal state after:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
x : ℤ
⊢ abv ↑x.natAbs = abv ↑x

Tactic:
obtain ⟨_, rfl | rfl⟩ := Int.eq_nat_or_neg x

Goal state after:
case inl
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
w✝ : ℕ
⊢ abv ↑(↑w✝).natAbs = abv ↑↑w✝

case inr
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
w✝ : ℕ
⊢ abv ↑(-↑w✝).natAbs = abv ↑(-↑w✝)
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
⊢ ∏ i ∈ s, f i < ∏ i ∈ s, g i

Tactic:
obtain ⟨i, hi, hilt⟩ := hlt
  rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
  · exact (hf i hi).le.trans hilt.le

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✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (embDomain { toFun := f, inj' := hf } s).prod h = s.prod fun a b ↦ h ({ toFun := f, inj' := hf } a) b

Tactic:
prod_embDomain

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
⊢ (s.prod fun a b ↦ h ({ toFun := f, inj' := hf } a) b) = 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
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ a ∈ Finset.subtype p f.support ↔ (⇑f ∘ Subtype.val) a ≠ 0

Tactic:
simp only [@mem_subtype _ _ (Classical.decPred p), mem_support_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ f ↑a ≠ 0 ↔ (⇑f ∘ Subtype.val) a ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∀ i ∈ {x ∈ s | f x = 1}, f i ≤ 1

Tactic:
simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
⊢ ∏ᶠ (i : p), f i = if h : p then f h else 1

Tactic:
by
  split_ifs with h
  · have : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
    exact finprod_unique f
  · have : IsEmpty p := ⟨h⟩
    exact finprod_of_isEmpty f

Goal state after: