mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case succ
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n✝ : ℕ
⊢ 2 ^ (n✝ + 1 + (n✝ + 1 - 1)) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1))) =
    2 ^ (2 * (n✝ + 1) - 1) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1)))

Tactic:
· simp [Nat.two_mul]

Goal state after:
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ ↑(n + 1) = a ^ ↑n * a

Tactic:
zpow_natCast,

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (n + 1) = a ^ ↑n * a
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (n + 1) = a ^ ↑n * a

Tactic:
zpow_natCast,

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (n + 1) = a ^ n * a
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |a ^ ↑m|ₘ = |a|ₘ ^ |↑m|

Tactic:
zpow_natCast,

Goal state after:
case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |a ^ m|ₘ = |a|ₘ ^ |↑m|
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
h₁,

Goal state after:
case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑db * ⅟↑da = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 ≤ a
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ a ≤ a / b

Tactic:
by
  simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
h₁,

Goal state after:
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑db * ⅟↑da = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
by
  rw [← mul_div_assoc] at h
  rwa [mul_comm b, ← div_le_iff₀ hc]

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

Goal state before:
pp: α : Type u
l : List α
a : α
ha : a ∈ l
ha' : a ≠ l.getLast ⋯
⊢ a ∈ l.dropLast

Tactic:
grind [dropLast_concat_getLast]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ a = D * f

Tactic:
h₁,

Goal state after:
M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ b = D * f
Module: Mathlib.Algebra.Order.Nonneg.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
b : { x // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ ↑b

Tactic:
obtain ⟨b, hb⟩ := b

Goal state after:
α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a b : α
hb : 0 ≤ b
⊢ toNonneg a ≤ ⟨b, hb⟩ ↔ a ≤ ↑⟨b, hb⟩
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
f g : α → Option β
h : ∀ (x : α), x ∈ [] → f x = g x
⊢ filterMap f [] = filterMap g []

Tactic:
simp_all [filterMap_cons]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f g : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (x : α), x ∈ tail✝ → f x = g x) → filterMap f tail✝ = filterMap g tail✝
h : ∀ (x : α), x ∈ head✝ :: tail✝ → f x = g x
⊢ filterMap f (head✝ :: tail✝) = filterMap g (head✝ :: tail✝)

Tactic:
simp_all [filterMap_cons]

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
by
    simp only [zpow_negSucc, inv_right_iff]
    apply pow_right h

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
by
  rw [← coe_inj]; simp [Rat.mkRat_eq_iff, h₁, h₂]; norm_cast

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
mul_right_comm,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * d * c ↔ b = a * d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
have : q.num * d = n * ↑q.den := by
    refine (divInt_eq_divInt_iff ?_ hd).mp ?_
    · exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
    · rwa [num_divInt_den]

Goal state after:
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den

Tactic:
apply Int.dvd_add

Goal state after:
case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den

case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₂.num * ↑q₁.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: z : ℤ
⊢ IsSquare z ∧ IsSquare (↑z).den ↔ IsSquare z

Tactic:
den_intCast,

Goal state after:
z : ℤ
⊢ IsSquare z ∧ IsSquare 1 ↔ IsSquare z
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑(↑q.den /. q.num) = (↑q)⁻¹

Tactic:
cast_divInt_of_ne_zero _ hq,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑↑q.den / ↑q.num = (↑q)⁻¹
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ a

Tactic:
simp only [gi.choice_eq]

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ b

Tactic:
simp only [gi.choice_eq]

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ gi.choice (u b ⊓ u c) ⋯

Tactic:
simp only [gi.choice_eq]

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ gi.choice ⊤ ⋯

Tactic:
simp only [gi.choice_eq]

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ i.pi s \ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a

Tactic:
simp only [mem_sdiff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not] at hx

Goal state after:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ x_1 ∈ i, eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1
⊢ x a ∈ t a
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Ici (sSup s) = ⋂ a ∈ s, Ici a

Tactic:
by rw [sSup_eq_iSup, Ici_iSup₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
⊢ CompleteLattice α

Tactic:
apply e.injective.completeLattice <;> intros

Goal state after:
case le
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_sSup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

case map_sInf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

case map_top
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : InfSet α
s : Set (WithTop α)
hs : ¬s ⊆ {⊤}
h's : BddBelow s
⊢ ¬(s ⊆ {⊤} ∨ ¬BddBelow s)

Tactic:
simp [hs, h's]

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

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
constructor
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a \ Ici b = Ico a b

Tactic:
rw [sdiff_eq, compl_Ici, Ici_inter_Iio]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α
s : Set ι
⊢ InjOn f s ↔ s.Pairwise fun x1 x2 ↦ f x1 ≠ f x2

Tactic:
by
  simp only [InjOn, Set.Pairwise, not_imp_not]

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ 0 ≤ c

Tactic:
← add_zero a.val,

Goal state after:
α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a + 0 ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ 0 ≤ c
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ ascFactorial 1 (k + 1) = (k + 1)!

Tactic:
rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ n.descFactorial k = n ! / (n - k)!

Tactic:
apply Nat.mul_left_cancel (n - k).factorial_pos

Goal state after:
n k : ℕ
h : k ≤ n
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case case3
n k : ℕ
ih₁ : n.ascFactorial ((k + 2) / 2) = n.ascFactorialBinary ((k + 2) / 2)
ih₂ : (n + (k + 2) / 2).ascFactorial ((k + 2 + 1) / 2) = (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)
⊢ n.ascFactorial k.succ.succ =
    n.ascFactorialBinary ((k + 2) / 2) * (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)

Tactic:
grind [ascFactorial_mul_ascFactorial]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1)).sign / ↑(if n + 1 = 0 then 1 else n + 1) = (↑(n + 1))⁻¹

Tactic:
if_neg n.succ_ne_zero,

Goal state after:
case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1)).sign / ↑(n + 1) = (↑(n + 1))⁻¹
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ ↑n)⁻¹ = (↑q ^ ↑n)⁻¹

Tactic:
zpow_natCast,

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ n)⁻¹ = (↑q ^ n)⁻¹
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
calc
    fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
      = fract (-(m₀ : k) / n) := by simp
    _ = fract ((m₁ : k) / n) := ?_
    _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
    _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_

Goal state after:
case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)

case inr.inr.calc_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ ↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ b⁻¹ < a⁻¹ * c

Tactic:
rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : ↑(Ico 0 1) → G
x : R
⊢ f ⟨Int.fract (x + 1), ⋯⟩ + ⌊x + 1⌋ • a = f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a + a

Tactic:
by
    simp [add_one_zsmul, add_assoc]

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : map f l₁ <+~ map f l₂
⊢ l₁ <+~ l₂

Tactic:
by
    obtain ⟨w, ⟨perm, sublist⟩⟩ := a
    obtain ⟨x, ⟨sublistₓ, mapₓ⟩⟩ := sublist_map_iff.mp sublist
    use x
    constructor
    · rw [mapₓ] at perm
      exact (map_perm_map_iff hf).mp perm
    · exact sublistₓ

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = n

Tactic:
by
  convert! List.count_replicate_self (a := a)
  rw [← coe_count, coe_replicate]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
induction h generalizing as with

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)

Tactic:
induction hst with
  | zero => simpa using huv
  | cons hab hst ih => simpa using ih.cons hab

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
subst hd
    simp [hl.1]

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [disjoint_cons_left] at h

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s.val.toList).Nodup

Tactic:
Multiset.coe_toList

Goal state after:
α : Type u_1
s : Finset α
⊢ s.val.Nodup
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t u : Finset α
h : Disjoint t u
⊢ Disjoint s (t.disjUnion u h) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
by
  simp only [disjoint_right, mem_disjUnion, or_imp, forall_and]

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

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹

Tactic:
@ne_comm _ b

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
intro hf i hi
    have := hf hi
    simp [Fin.ext_iff] at this

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

Goal state before:
pp: m n : ℕ
h : n = m
⊢ (castOrderIso h).symm = castOrderIso ⋯

Tactic:
subst h; rfl

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

Goal state before:
pp: m n : ℕ
h : n = m
⊢ (castOrderIso h).toEquiv = Equiv.cast ⋯

Tactic:
subst h; rfl

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ ↑↑a = a.castSucc

Tactic:
by
  ext
  exact val_cast_of_lt (Nat.lt_succ_of_lt a.is_lt)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ f x = f y → x = y

Tactic:
contrapose

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ ¬x = y → ¬f x = f y
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a.succ.castPred ha ≤ b ↔ a < b

Tactic:
castPred_le_iff,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a.succ ≤ b.castSucc ↔ a < b
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten

Tactic:
by
  simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]

Goal state after: