mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
s : Finset M
s_card : s.card = n
s_ind : LinearIndepOn R id ↑s
⊢ ∃ v, LinearIndependent R v

pp: case refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
· exact ⟨_, s_ind.comp _ (s.equivFinOfCardEq s_card).symm.injective⟩

Goal state after:
case refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) ≤ toNat ↑n
⊢ finrank R M ≤ n

pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ Module.rank R M < ℵ₀

pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀

Tactic:
toNat_natCast

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) ≤ n
⊢ finrank R M ≤ n

case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ Module.rank R M < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) < toNat ↑n
⊢ finrank R M < n

pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀

Tactic:
toNat_natCast

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) < n
⊢ finrank R M < n

case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ toNat ↑n < toNat (Module.rank R M)

pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Tactic:
toNat_natCast

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ n < toNat (Module.rank R M)

case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀
Module: Mathlib.GroupTheory.MonoidLocalization.Finite

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : S.FG
⊢ Monoid.FG (Localization S)

Tactic:
rw [← Monoid.fg_iff_submonoid_fg] at hS; exact Monoid.fg_of_surjective mkHom mkHom_surjective

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
rw [← encard_union_add_encard_inter]

Goal state after:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case succ
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ↑n.succ ≤ s.encard
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

Tactic:
simp only [Nat.cast_succ] at *

Goal state after:
case succ
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n + 1
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case empty
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ ∅, x i = 1
h2 : ∀ i ∈ ∅, Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
    exact this ▸ one_mem H

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
apply Finite.equivFin

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ normalizer S

Tactic:
cases nonempty_fintype S

Goal state after:
case intro
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
⊢ x ∈ normalizer S
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
have hft := ht.fintype

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ op x • ↑s = op y • ↑s ↔ y * x⁻¹ ∈ s

Tactic:
rw [Set.ext_iff]
  simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [mul_inv_cancel]
    exact s.one_mem
  · intro h z
    rw [← inv_mul_cancel_left y x⁻¹]
    rw [← mul_assoc]
    exact s.mul_mem_cancel_right h

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ (leftRel (s.subgroupOf t)) ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩ ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩

Tactic:
rw [leftRel_apply]
        change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
        have key : f b = f c :=
          congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
        rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 1 ↔ ∃ a, s = {a}

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩

Goal state after:
α : Type u_1
s : Set α
h : s.ncard = 1
⊢ ∃ a, s = {a}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Infinite
⊢ ∀ x ∉ s, ¬insert x s = t

Tactic:
rintro x - rfl

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
ht : (insert x s).Infinite
⊢ False
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
⊢ ∀ (a : ↥(H ⊔ N)), ∃ a_1, φ a_1 = Quotient.mk'' a

Tactic:
by
      rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
      rw [← SetLike.mem_coe] at hy
      rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy
      rcases hy with ⟨h, hh, n, hn, rfl⟩
      simp only [SetLike.mem_coe] at hn
      use ⟨h, hh⟩
      refine Quotient.eq.mpr ?_
      simp [leftRel_apply, inclusion, mem_subgroupOf, hn]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', mrange f = f'.mgraph

Tactic:
obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : Set.range ⇑f = graphOn f' univ
⊢ ∃ f', mrange f = f'.mgraph
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : (Set.range g)ᶜ ⊆ {x}
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
simp only [Set.subset_def, Set.mem_compl_iff] at hx

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases ha : a ∈ Set.range g <;> by_cases hb : b ∈ Set.range g

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Function.Surjective mk

Tactic:
by
  rintro ⟨x⟩
  exact ⟨x, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x ↦ x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x ↦ x.toSetoid) c = r
⊢ ((fun x ↦ x.toSetoid) c) x y

Tactic:
exact h c hS

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom ≤ ringConGen (r on ⇑f)

Tactic:
· rw [← comap_nonUnitalRingHomComp]
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ f (∑ j, Pi.single j (x j)) = f x

Tactic:
Finset.univ_sum_single

Goal state after:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ f x = f x
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ioo a (succ b)) = ↑(Ioc a b)

Tactic:
simpa using Set.Ioo_succ_right_eq_Ioc_of_not_isMax hb _

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed ⇑(partialSups d)

Tactic:
disjointed_partialSups

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed d
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I✝ J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst✝ : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ ∈ I

Tactic:
exact mul_sub_mul_mem I h₁ h₂

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = span {p}

Tactic:
rw [or_iff_not_imp_left, ← forall_congr' isPrime_iff_of_isPrincipalIdealRing,
    ← or_iff_not_imp_left, or_iff_right_of_imp]

Goal state after:
α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P = ⊥ → P.IsPrime
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊤

Tactic:
rw [← h]; simp

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'

Tactic:
· rintro ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩
      exact mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
⊢ univ ∈ {t | q t}

Tactic:
by simpa [q] using uni

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

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ ⋃ i, Iic (f i) = univ

Tactic:
by
  refine Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)
  gcongr
  exact Iio_subset_Iic_self

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : Injective m
s : Set α
hs : s ∈ f
⊢ m ⁻¹' m '' s ⊆ s

Tactic:
by
        simp only [preimage_image_eq s h, Subset.rfl]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ (Prod.mk '' u).seq t ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
Set.prod_image_seq_comm

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ ((fun b a ↦ (a, b)) '' t).seq u ∈ (map (fun b a ↦ (a, b)) g).seq f
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
by
  rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
⊢ N ≤ N₀

Tactic:
by_contra h₃

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ cof α < ℵ₀ ↔ cof α ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
⊢ cof α ≤ 1
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hS : (restrictScalars R S).FG
⊢ S.FG

Tactic:
obtain ⟨s, e⟩ := hS

Goal state after:
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ S.FG
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ cof α < ℵ₀ ↔ cof α ≤ 1

Tactic:
by
  refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩
  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
  have hf : s.Finite := by
    rw [Set.Finite, ← mk_lt_aleph0_iff]
    exact hs'.trans_lt h
  obtain ⟨t, ht, ht'⟩ := hf.exists_subsingleton_isCofinal hs
  apply (cof_le ht').trans
  simpa

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ IsCompactElement s → s.FG

Tactic:
· intro h
    rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
    -- s is the Sup of the spans of its elements.
    have sSup' : s = sSup (sp '' ↑s) := by
      rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
    -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
    obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
    have ssup : s = u.sup id := by
      suffices u.sup id ≤ s from le_antisymm husup this
      rw [sSup', Finset.sup_id_eq_sSup]
      exact sSup_le_sSup huspan
    obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
    rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
      ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup
    exact ⟨t, ssup⟩

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLT α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, (a₁ • b ≤ a₂ • b ∧ ∃ i, (a₁ • b) i < (a₂ • b) i) → a₁ < a₂

Tactic:
rintro b hb _a₁ _a₂ ⟨-, i, hi⟩

Goal state after:
α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLT α (β i)
b : (i : ι) → β i
hb : 0 ≤ b
_a₁ _a₂ : α
i : ι
hi : (_a₁ • b) i < (_a₂ • b) i
⊢ _a₁ < _a₂
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} a

Tactic:
exact isLUB_singleton

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ b ∈ {a}

Tactic:
subst hda

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hdn : {a}.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) {a}
hb : IsLUB {a} b
⊢ b ∈ {a}
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
b : α
hb : b ∈ s
⊢ (f ⁻¹' s).Nonempty

Tactic:
obtain ⟨c, rfl⟩ := hs hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
c : α
hb : f c ∈ s
⊢ (f ⁻¹' s).Nonempty