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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ b.reindexRange ⟨b i, ⋯⟩ = ↑⟨b i, ⋯⟩

Tactic:
exact b.reindexRange_self i

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Iio a) = Iio ↑a

Tactic:
by
  rw [← attachFin_Iio, map_valEmbedding_attachFin]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case zero
α : Type u
v : Fin (0 + 1) → α
i : Fin (0 + 1)
⊢ (if h : ↑i + ↑i + 1 < 0 + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (0 + 1), ⋯⟩) = v (i + i + 1)

Tactic:
obtain ⟨i, hi⟩ := i

Goal state after:
case zero
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi : i < 0 + 1
⊢ (if h : ↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi⟩ + ⟨i, hi⟩ + 1)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : x ∈ mulSupport fun a ↦ ∏ b ∈ s, f a b
⊢ ∃ i ∈ s, ¬f x i = 1

Tactic:
contrapose! hx

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ x ∉ mulSupport fun a ↦ ∏ b ∈ s, f a b
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k

Tactic:
rw [Finset.prod_image']

Goal state after:
case eq
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∀ i ∈ s, ∏ y ∈ s with f y = ?m.36 i, g y = ∏ j ∈ s with ?m.36 j = ?m.36 i, g j

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ β → α
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b

Tactic:
rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hcd : ∃ m n, m • p + c = n • p + d
k l : ℕ
hab : k • p + a = l • p + b
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)

Tactic:
rcases hcd with ⟨m, n, hcd⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
i : ι
⊢ x i = y i

Tactic:
exact hinj congr($this i)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ span R (v '' univ) ⊓ f.ker ≤ ⊥

Tactic:
Finsupp.span_image_eq_map_linearCombination,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ map (Finsupp.linearCombination R v) (Finsupp.supported R R univ) ⊓ f.ker ≤ ⊥
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inl
n a b : ℕ
h : a ≡ b [MOD n]
h0 : a ≤ b
⊢ n ∣ b - a

Tactic:
exact (modEq_iff_dvd' h0).mp h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha : a • v i ∈ span R (v '' (univ \ {i}))
⊢ a = 0

Tactic:
Finsupp.span_image_eq_map_linearCombination,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha : a • v i ∈ map (Finsupp.linearCombination R v) (Finsupp.supported R R (univ \ {i}))
⊢ a = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ ↑c * ↑m ∣ ↑c * (↑b - ↑a) → ↑m ∣ ↑b - ↑a

Tactic:
exact fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ s ∪ t

Tactic:
apply Set.subset_union_left

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a✝ b✝ c d : ℕ
co : n.Coprime m
a b : ℕ
⊢ a ≡ b [MOD n.gcd m]

Tactic:
convert! @modEq_one a b

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

Goal state before:
pp: α : Type u_3
⊢ 1 ≤ card α ↔ Nonempty α

Tactic:
by
  simp [Order.one_le_iff_ne_zero, card_eq_zero_iff_empty]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (∑ i ∈ insert a s, g i • ⇑i) 1

Tactic:
Finset.sum_insert has,

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (g a • ⇑a + ∑ x ∈ s, g x • ⇑x) 1
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1

Tactic:
simpa only [one_mul] using mul_left_not_lt 1 h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ LinearIndependent R (-v) ↔ LinearIndependent R v

Tactic:
by
  refine ⟨fun h ↦ ?_, LinearIndependent.neg⟩
  simpa using h.neg

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y

pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}

Tactic:
· rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ ∑ i ∈ t.preimage Subtype.val ⋯, g ↑i • v ↑i = 0

Tactic:
t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ ∑ x ∈ t, g x • v x = 0

case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ ∀ x ∈ t, x ∉ range Subtype.val → g x • v x = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ y

pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

pp: case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}

Tactic:
· rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z

case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s

Tactic:
← ENat.card_sum,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card (↑(t \ s) ⊕ ↑s) ≤ 0 + ENat.card ↑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
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a : α
ha✝ : a ∈ s.toFinset
ha : a ∈ s
⊢ f'' a ha✝ ∈ t

Tactic:
exact hf a ha

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (t ∩ s).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
add_lt_add_iff_left

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s \ t).ncard < (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard + s.ncard = Nat.card α

Tactic:
rw [add_comm, ncard_add_ncard_compl s hs hsc]

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

Goal state before:
pp: case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x y : N
h : rel x y
a b : M
fa : f a = x
fb : f b = y
⊢ rel (f a) (f b)

Tactic:
fa,

Goal state after:
case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x y : N
h : rel x y
a b : M
fa : f a = x
fb : f b = y
⊢ rel x (f b)
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
fa,

Goal state after:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) (f.symm w * f.symm y) b
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
by
  simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
by_cases hι : Nonempty ι

Goal state after:
case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ^[n + 1] i < j

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMonoid A
inst✝ : HasMulAntidiagonal A
n : A
xy : A × A
⊢ xy.swap ∈ mulAntidiagonal n ↔ xy ∈ mulAntidiagonal n

Tactic:
by
  simp [mul_comm]

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)

Tactic:
by
  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥

Tactic:
by_cases H : r = 0

Goal state after:
case pos
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥

case neg
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ a * a * b + a * b * a = 0

Tactic:
rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), n * n.choose i = n * 2 ^ n

Tactic:
← mul_sum,

Goal state after:
n : ℕ
h : ¬n = 0
⊢ n * ∑ i ∈ range (n + 1), n.choose i = n * 2 ^ n
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ ∑ ij ∈ antidiagonal (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)

Tactic:
| succ n hn =>

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
simp only [Filter.Frequently, hl.eventually_iff]

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
m : α → Filter β
⊢ (pure a).bind m = m a

Tactic:
simp only [bind, map_pure, join_pure]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
⊢ f ⊔ g ≤ᶠ[l] h

Tactic:
by
  filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ CommGroup α

Tactic:
apply e.injective.commGroup _

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddMonoid M
inst✝ : IsAddTorsionFree M
n : ℕ
x : M
hx : n • x = 0
⊢ n = 0 ∨ x = 0

Tactic:
contrapose! hx

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddMonoid M
inst✝ : IsAddTorsionFree M
n : ℕ
x : M
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : IsAddTorsionFree G
n : ℤ
x : G
hx : n • x = 0
⊢ n = 0 ∨ x = 0

Tactic:
contrapose! hx

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : IsAddTorsionFree G
n : ℤ
x : G
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

Tactic:
by
    simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLT α β
h : -a • b₂ < -a • b₁
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.1 < _b.1
⊢ _a₁ ≤ _a₂

pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.2 < _b.2
⊢ _a₁ ≤ _a₂

Tactic:
· exact le_of_smul_le_smul_right h.1 h₁

Goal state after:
case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.2 < _b.2
⊢ _a₁ ≤ _a₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂

Tactic:
exact smul_lt_smul_of_pos_left hb ha

Goal state after: