mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
⊢ Quotient.map' (fun b ↦ f (Quotient.map' id ⋯ (Quotient.mk'' a)) * ↑b) ⋯
      (Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ (Quotient.mk'' a)) =
    Quotient.mk'' a

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ Quotient.map' (fun b ↦ f (Quotient.map' id ⋯ (Quotient.mk'' a)) * ↑b) ⋯
      (Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ (Quotient.mk'' a)) =
    Quotient.mk'' a
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 : α
b : ↥t
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (Quotient.map' id ⋯ (Quotient.map' (fun b ↦ f (Quotient.mk'' a) * ↑b) ⋯ (Quotient.mk'' b)),
      Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯
        (Quotient.map' (fun b ↦ f (Quotient.mk'' a) * ↑b) ⋯ (Quotient.mk'' b))) =
    (Quotient.mk'' a, Quotient.mk'' b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (Quotient.map' id ⋯ (Quotient.map' (fun b ↦ f (Quotient.mk'' a) * ↑b) ⋯ (Quotient.mk'' b)),
      Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯
        (Quotient.map' (fun b ↦ f (Quotient.mk'' a) * ↑b) ⋯ (Quotient.mk'' b))) =
    (Quotient.mk'' a, Quotient.mk'' b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s)) a b → (leftRel (H.subgroupOf t)) ((inclusion h) a) ((inclusion h) b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s)) a b → (leftRel (H.subgroupOf t)) ((inclusion h) a) ((inclusion h) b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ (leftRel (s.subgroupOf H)) a b → (leftRel (t.subgroupOf H)) (id a) (id b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ (leftRel (s.subgroupOf H)) a b → (leftRel (t.subgroupOf H)) (id a) (id b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ (leftRel s) a b → (leftRel t) (id a) (id b)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ (leftRel s) a b → (leftRel t) (id a) (id b)
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:
[

Goal state after:
α : 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₂
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:
[

Goal state after:
α : 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₂
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ univ = ⋃ x, Quotient.out x • ↑H

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ univ = ⋃ x, Quotient.out x • ↑H
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

Tactic:
[

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ s.ncard + t.ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty

Tactic:
rw [← ncard_union_add_ncard_inter s t] at h'
  replace h := (ncard_lt_card h).trans_le h'
  rwa [lt_add_iff_pos_right, ncard_pos] at h

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

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

Tactic:
[

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

Goal state before:
pp: α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_2
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
x : α
⊢ x ∉ s ∧ insert x hs.toFinset = ht.toFinset ↔ x ∉ s ∧ insert x s = t

Tactic:
simp [Finset.ext_iff, Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : s.Finite
⊢ 1 < s.ncard

Tactic:
rw [← Set.finite_coe_iff] at hs_finite

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : Finite ↑s
⊢ 1 < s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
h : s.ncard = 1
⊢ False

Tactic:
by simp [h] at he

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
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' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y

Tactic:
[

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' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Add R'
inst✝¹ : Mul R'
c✝ d : RingCon R
inst✝ : Subsingleton R
c c' : RingCon R
r r' : R
⊢ c r r' ↔ c' r r'

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Add R'
inst✝¹ : Mul R'
c✝ d : RingCon R
inst✝ : Subsingleton R
c c' : RingCon R
r r' : R
⊢ c r r' ↔ c' r r'
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ Nontrivial (RingCon R) ↔ Nontrivial R

Tactic:
[

Goal state after:
case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ Nontrivial (RingCon R) ↔ Nontrivial R
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R

Tactic:
[

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R
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 ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨆ i ∈ I, (single R φ i).range) (⨆ i ∈ J, (single R φ i).range)

Tactic:
by
  refine
    Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
      (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_
  simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
    funext_iff]
  rintro b ⟨hI, hJ⟩ i
  classical
    by_cases hiI : i ∈ I
    · by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ
    · exact hI i hiI

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁹ : Semiring R
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type u_1
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
i : ι
x : φ i
⊢ ((lsum R φ S) f) (Pi.single i x) = (f i) x

Tactic:
[

Goal state after:
R : Type u
M : Type v
ι : Type x
inst✝⁹ : Semiring R
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type u_1
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
i : ι
x : φ i
⊢ ((lsum R φ S) f) (Pi.single i x) = (f i) x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (pred b)) = Ioc a b

Tactic:
Ioc_pred_right_of_not_isMin h.not_isMin,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b
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 ι
i : ι
⊢ single R φ i = pi (diag i)

Tactic:
ext x j
  convert! (update_apply 0 x i j _).symm
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0

Tactic:
this

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : 0 + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ ↑(insert a (Ioc a b)) = ↑(Ioc (pred a) b)

Tactic:
simpa using Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin h ha

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
this

Goal state after:
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ ∑ i, x (Sum.inl i) • single (Sum.inl i) 1 ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1

Tactic:
[

Goal state after:
case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = s.toFinset.inf fun i ↦ a ⊔ id i

Tactic:
Finset.inf_eq_iInf

Goal state after:
case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s.toFinset, a ⊔ id a_1
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s.toFinset, a ⊔ id a_1

Tactic:
[

Goal state after:
case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s.toFinset, a ⊔ id a_1
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
x✝ : ↑(Set.Iic i)
j : ι
hj : j ∈ Set.Iic i
⊢ ↑⟨j, hj⟩ ∈ Iic i

Tactic:
simpa only [mem_Iic, Set.mem_Iic] using hj

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f = partialSups g
⊢ ⨆ i, f i = ⨆ i, g i

Tactic:
[

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f = partialSups g
⊢ ⨆ i, f i = ⨆ i, g i
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S 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 →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range = e₂.graph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S 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 →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = e₁ x.1
he₂ : ∀ (x : I × H), x ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range ↔ x.2 = e₂ x.1
⊢ e₁ h = i ↔ e₂ i = h
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k

Tactic:
[

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i < a + 1, f i = (∏ i < a, f i) * f a

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i < a + 1, f i = (∏ i < a, f i) * f a
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i ≤ a + 1, f i = (∏ i ≤ a, f i) * f (a + 1)

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i ≤ a + 1, f i = (∏ i ≤ a, f i) * f (a + 1)
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ i, ∏ j > i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ i, ∏ j > i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0
⊢ IsMin (pred^[n + 1] i0)

Tactic:
exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m k, f i

Tactic:
← Ioc_union_Ioc_eq_Ioc hmn hnk,

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m n ∪ Ioc n k, f i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ (if 0 ≤ toZ hι.some i then succ^[(toZ hι.some i).toNat] hι.some else pred^[(-toZ hι.some i).toNat] hι.some) = i

Tactic:
[

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ (if 0 ≤ toZ hι.some i then succ^[(toZ hι.some i).toNat] hι.some else pred^[(-toZ hι.some i).toNat] hι.some) = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
⊢ (if 0 ≤ toZ hι.some i then succ^[(toZ hι.some i).toNat] hι.some else pred^[(-toZ hι.some i).toNat] hι.some) = i

Tactic:
[

Goal state after:
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
⊢ (if 0 ≤ toZ hι.some i then succ^[(toZ hι.some i).toNat] hι.some else pred^[(-toZ hι.some i).toNat] hι.some) = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ hι.some (if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) = n

Tactic:
[

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ hι.some (if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) = n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ hι.some (if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) = n

Tactic:
[

Goal state after:
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ hι.some (if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) = n
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ ↑(List.Nat.antidiagonal n).reverse = ↑(List.Nat.antidiagonal n)

Tactic:
coe_reverse

Goal state after:
n : ℕ
⊢ ↑(List.Nat.antidiagonal n) = ↑(List.Nat.antidiagonal n)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Tactic:
[

Goal state after:
n : ℕ
⊢ antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯