mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x ∈ ⊥
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ P N

Tactic:
exfalso

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x ∈ ⊥
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : 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
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t

Tactic:
exact (hf₀s x hx h).1

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
⊢ x ∈ normalizer S

Tactic:
by
  have := Classical.propDecidable; cases nonempty_fintype S
  exact fun n =>
    ⟨h n, fun h₁ =>
      have heq : (fun n => x * n * x⁻¹) '' S = S :=
        Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
          (by rw [Set.card_image_of_injective S conj_injective])
      have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
      let ⟨y, hy⟩ := this
      conj_injective hy.2 ▸ hy.1⟩

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
· rw [ncard_insert_of_notMem h hs, if_neg h]

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
convert! Nat.zero_le _

Goal state after:
case e'_3
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
h : b ∈ {a}
⊢ a ∈ s

Tactic:
rwa [← mem_singleton_iff.mp h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H),
    ((fun i ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁)) = fun i ↦
        quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
funext_iff,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    ((fun i ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) = fun i ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
funext_iff,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0

Tactic:
simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v + w) i.succ = vecCons (x + vecHead w) (v + vecTail w) i.succ

Tactic:
simp [vecHead, vecTail]

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

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Tactic:
convert! Nat.zero_le _

Goal state after:
case e'_3
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ s.ncard = 0
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0

Tactic:
simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ

Tactic:
simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0

Tactic:
simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ

Tactic:
simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0

Tactic:
simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ

Tactic:
simp [vecHead, vecTail]

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₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
exact ⟨
  { toFun := e₁
    map_mul' := e₁.map_mul'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ f : M →* P
x✝ : ↥(MonoidHom.mrange (kerLift f))
w : P
z : (ker f).Quotient
hz : (kerLift f) z = w
⊢ (kerLift f).mrangeRestrict z = ⟨w, ⋯⟩

Tactic:
rcases hz with ⟨⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ f : M →* P
x✝ : ↥(MonoidHom.mrange (kerLift f))
z : (ker f).Quotient
⊢ (kerLift f).mrangeRestrict z = ⟨(kerLift f) z, ⋯⟩
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ ⨆ i, (single R φ i).range = ⊤

Tactic:
by
  simpa using iInf_ker_proj_le_iSup_range_single R φ Set.finite_univ isCompl_top_bot.codisjoint

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
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 ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ∘ₗ
      codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ =
    id

pp: case refine_3
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 ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id

Tactic:
· simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]
    ext b ⟨j, hj⟩
    simp only [dif_pos,
      LinearMap.coe_proj, LinearMap.pi_apply]
    rfl

Goal state after:
case refine_3
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 ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ (P.mapQ S (↑f ∘ₛₗ ↑e) ⋯) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)

Tactic:
rw [mapQ_comp, LinearMap.comp_apply]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
τ : Type u_4
π : τ → Type u_5
inst✝ : (t : τ) → SemilatticeSup (π t)
f : ι → (t : τ) → π t
i : ι
t : τ
⊢ (partialSups f) i t = (partialSups fun x ↦ f x t) i

Tactic:
simp only [partialSups_apply, Finset.sup'_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
⊢ toZ i0 (succ^[n] i0) = ↑n

Tactic:
by
  let m := (toZ i0 (succ^[n] i0)).toNat
  have h_eq : succ^[m] i0 = succ^[n] i0 := iterate_succ_toZ _ (le_succ_iterate _ _)
  by_cases hmn : m = n
  · nth_rw 2 [← hmn]
    rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
    exact Int.natCast_nonneg _
  suffices IsMax (succ^[n] i0) from absurd this hn
  exact isMax_iterate_succ_of_eq_of_ne h_eq.symm (Ne.symm hmn)

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

Goal state before:
pp: case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j

Tactic:
rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]

Goal state after:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ pred^[(-toZ i0 i).toNat] i0 ≤ pred^[(-toZ i0 j).toNat] i0
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i, if i ∈ Icc a b then f i else 1) = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
prod_fin_eq_prod_range

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Icc a b then f ⟨i, h⟩ else 1 else 1) =
    ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ (∏ i, if i ∈ Iic a then f i.succ / f i.castSucc else 1) = f a.succ / f 0

Tactic:
prod_fin_eq_prod_range

Goal state after:
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Iic a then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1 else 1) =
    f a.succ / f 0
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ ¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I

Tactic:
simp_rw [Ideal.isPrime_iff, not_and_or, Ne, Classical.not_not, not_forall, not_or]
  exact
    or_congr Iff.rfl
      ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ =>
        ⟨x, y, hxy, hx, hy⟩⟩

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∀ (i : ι), ∃ a, a * r i = x✝ i) ↔ ∃ a, a * r = x✝

Tactic:
funext_iff,

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∀ (i : ι), ∃ a, a * r i = x✝ i) ↔ ∃ a, ∀ (x : ι), (a * r) x = x✝ x
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
B : FilterBasis α
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun s ↦ 𝓟 ↑s

Tactic:
rintro ⟨U, U_in⟩ ⟨V, V_in⟩

Goal state after:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨U, U_in⟩) ((fun s ↦ 𝓟 ↑s) z) ∧
      (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨V, V_in⟩) ((fun s ↦ 𝓟 ↑s) z)
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s

Tactic:
simp_rw [mem_kernMap_iff_compl, compl_compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Disjoint g₁ g₂
⊢ Disjoint (comap m g₁) (comap m g₂)

Tactic:
by
  simp only [disjoint_iff, ← comap_inf, h.eq_bot, comap_bot]

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

Goal state before:
pp: case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a

pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
· exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ i ∈ s, Ici i
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x✝ : Set α
⊢ ∀ᶠ (x : α) in f, x ∈ x✝ → p x

Tactic:
by filter_upwards [h] with _ pa _ using pa

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩

Goal state after:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ IsDirectedOrder ↑s

Tactic:
directedOn_iff_directed

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirectedOrder ↑s
Module: Mathlib.Order.SuccPred.InitialSeg

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

Tactic:
simp [wcovBy_iff_eq_or_covBy]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

Tactic:
rw [← f.apply_covBy_apply_iff] at hb
    exact h _ hb

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
t : Finset M
⊢ IsCompactElement (⨆ x ∈ ↑t, R ∙ x)

Tactic:
← supr_rw,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
t : Finset M
⊢ IsCompactElement (⨆ x ∈ t, sp x)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
⊢ a < b → f a < f b

Tactic:
induction b using SuccOrder.limitRecOn with

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: a : Ordinal.{u}
f : ↑(Iio a) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ ⨆ i, f i + 1 = ⨆ i, f i

Tactic:
by
  have := ha.noMaxOrder_Iio
  exact iSup_add_one hf

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o < (succ c).ord

Tactic:
lt_ord,

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o.card < succ c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ Ordinal.lift.{u, 0} o < ℵ₀.ord

Tactic:
lt_ord,

Goal state after:
o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ (Ordinal.lift.{u, 0} o).card < ℵ₀
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord

Tactic:
lt_ord,

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ (Ordinal.lift.{u, v} a).card < lift.{u, v} c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ a < c.ord, a + 1 < c.ord

Tactic:
lt_ord,

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ (a : Ordinal.{u_1}), a.card < c → (a + 1).card < c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb
    · refine eq_of_forall_lt_iff fun c ↦ ?_
      rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
    · suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
      apply Nat.div_eq_of_lt
      grind

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0

Tactic:
rcases le_one_iff.1 hb with (rfl | rfl)
    · exact log_zero_left o
    · exact log_one_left o

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a = nfp f a

Tactic:
by
  apply le_antisymm
  · rw [Ordinal.iSup_le_iff]
    intro n
    rw [← List.length_replicate (n := n) (a := Unit.unit), ← List.foldr_const f a]
    exact Ordinal.le_iSup _ _
  · apply Ordinal.iSup_le
    intro l
    rw [List.foldr_const f a l]
    exact Ordinal.le_iSup _ _

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsSuccLimit (ω_ o)

Tactic:
rw [← ord_aleph]

Goal state after:
o : Ordinal.{u_1}
⊢ IsSuccLimit (ℵ_ o).ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases le_or_gt ℵ₀ b with hb | hb
    · rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
by
  have := lift_card_iSup_le_sum_card f
  rwa [Cardinal.lift_id'] at this

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ (o'.blsub fun i hi ↦ f (g i hi) ⋯) = a

Tactic:
@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)

Goal state after:
case refine_2
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o.blsub f = a

case refine_2.hg
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o'.blsub g = o