mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
n : ℕ
x : M
hn : 0 < n
h : x < 1
⊢ x ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩
  rw [pow_succ]
  exact mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a⁻¹ * b⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1

Tactic:
by
  rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y

Tactic:
← Nat.mul_div_cancel' h,

Goal state after:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑(a.gcd b * (n / a.gcd b)) = a * x + b * y
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q - 1 ≤ ↑n - 1

Tactic:
rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: case one
α : Type u
d : α
x : WithOne α
⊢ unoneD d x = unoneD d 1 ↔ x = 1 ∨ x = ↑d ∧ 1 = 1 ∨ x = 1 ∧ 1 = ↑d

Tactic:
simp [unoneD_eq_iff, or_comm]

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: case coe
α : Type u
d : α
x : WithOne α
a✝ : α
⊢ unoneD d x = unoneD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = 1 ∨ x = 1 ∧ ↑a✝ = ↑d

Tactic:
simp [unoneD_eq_iff, or_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
⊢ False

Tactic:
rcases exists_pair_ne R with ⟨x, y, xy⟩

Goal state after:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False

Tactic:
rcases exists_pair_ne R with ⟨x, y, xy⟩

Goal state after:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤

Tactic:
exact add_ne_top

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
rw [← not_iff_not, not_or]; exact add_ne_top

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a - c - (b - c) = a - b

Tactic:
by
  rw [tsub_tsub, add_tsub_cancel_of_le h]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
a✝ : Multiplicative G
⊢ ↑a✝ ≤ exp (↑a✝).log

Tactic:
· rfl

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
⊢ x ≤ exp x.log

Tactic:
cases x
  · simp
  · rfl

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

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ ⅟(a * b) * a * b = 1

Tactic:
by rw [mul_assoc, invOf_mul_self]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r₂✝ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 ↦ r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 ↦ r₂✝ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x✝¹.1 r₁
hqr₁ : r x✝.1 r₁
r₂ : β
hdr₂ : r₂ ∈ d₂
hpr₂ : r₂✝ x✝¹.2 r₂
hqr₂ : r₂✝ x✝.2 r₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q ↦ r p.1 q.1 ∧ r₂✝ p.2 q.2) x✝¹ z ∧ (fun p q ↦ r p.1 q.1 ∧ r₂✝ p.2 q.2) x✝ z

Tactic:
exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) ≤
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))

Tactic:
gcongr _ * (_ + _ + ?_)

Goal state after:
case ha
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 0 ≤ 2 ^ n

case h₂
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
Module: Mathlib.Algebra.Order.Ring.Basic

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

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:
· rfl

Goal state after:
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)))
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y

Tactic:
have := hφ (ψts ys) (ψts xs) ψyx
    rw [φψs.eq ys, φψs.eq xs] at this
    induction le_antisymm l this
    exact le_refl _

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2) ↔ WellFoundedGT α

Tactic:
by
  simp_rw [isWellFounded_iff]
  convert! wellFounded_liftOn₂'_iff with ⟨_⟩ ⟨_⟩
  exact fun _ _ _ _ h₁ h₂ ↦ propext
    ⟨fun h ↦ (h₂.2.trans_lt h).trans_le h₁.1, fun h ↦ (h₂.1.trans_lt h).trans_le h₁.2⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
by
  ext
  simp [and_assoc]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
by
  ext
  simp [and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
exact nonempty_Ico

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ (Icc a b \ {a}) \ {b} = Ioo a b

Tactic:
Icc_sdiff_left,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Ioc a b \ {b} = Ioo a b
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
⊢ MapsTo (Sum.elim f g) (sumEquiv.symm s) t

Tactic:
rintro (a | b) <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨rfl⟩

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

Goal state before:
pp: case mp.nil
α : Type u_1
a b : List α
⊢ [] = []

pp: case mp.cons
α : Type u_1
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x1 x2 ↦ x1 = x2) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝

Tactic:
· rfl

Goal state after:
case mp.cons
α : Type u_1
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x1 x2 ↦ x1 = x2) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
use l'

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ Forall₂ (fun a c ↦ R a (f c)) l₁ l' ∧ l' <+ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr.nil.nil
α : Type u
hα : Subsingleton α
hl : [].length = [].length
⊢ [] = []

pp: case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

pp: case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

pp: case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Tactic:
· rfl

Goal state after:
case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

pp: case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

pp: case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

pp: case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b

Tactic:
· rfl

Goal state after:
case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b

Tactic:
· exact Option.mem_toList.1 (p.symm.subset <| by simp)

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
⊢ l.head! = l.head?.getD default

Tactic:
by
  cases l <;> rfl

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

Goal state before:
pp: case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!

Tactic:
· rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
· simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]

Goal state after:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Tactic:
exact eq_of_mem_replicate h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ (take n L).prod * a * (drop (n + 1) L).prod = L.prod * (L[n]⁻¹ * a)

Tactic:
rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]

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

Goal state before:
pp: α : Type u
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
⊢ Injective (foldl comp f l)

Tactic:
induction l generalizing f with
  | nil => exact hf
  | cons lh lt l_ih =>
    apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
    apply Function.Injective.comp hf
    apply hl _ mem_cons_self

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

Goal state before:
pp: q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ den ^ n ≠ 0

Tactic:
simp [Nat.pow_eq_zero, hd]

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

Goal state before:
pp: case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [hd]
    simp

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

Goal state before:
pp: q : ℚ
h : q.isInt = true
⊢ q = ↑q.num

Tactic:
rw [Rat.isInt, Nat.beq_eq_true_eq] at h
  exact (Rat.coe_int_num_of_den_eq_one h).symm

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)

Tactic:
congr 2
    rw [← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_def, if_neg ‹_›]
    congr

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num * ↑q.den = ↑q.num * ↑p.den

Tactic:
norm_cast at hpq ⊢

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a a' : α
h : a = a'
b : α
⊢ a • b = a' * b

Tactic:
subst h

Goal state after:
α : Type u_2
inst✝ : Mul α
a b : α
⊢ a • b = a * b
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
· apply h.eq_tsub_of_add_eq
    rw [← add_mul, tsub_add_cancel_of_le hba]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
⊢ l (sSup s) = ⨆ a ∈ s, l a

Tactic:
simp only [sSup_eq_iSup, gc.l_iSup]

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

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
by
  obtain rfl := propext pq
  congr with x
  apply f

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
s : Set α
b : α
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa only [inf_comm] using inf_sSup_eq s b minAx

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
by
  rw [iSup, minAx.sSup_inf_eq, iSup_range]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
calc
      _ ≤ ⨆ i : ULift.{u} Bool, ⨅ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by
        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2
      _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
⊢ lhs ≤ rhs

Tactic:
have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
this : ∀ (a : α), ∃ b, rhs < g a b
⊢ lhs ≤ rhs
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' t) ≤ sInf (f '' s)

Tactic:
by gcongr; exacts [ht, hs.image f]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ p < q → ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
by
  simpa [← coe_ssubset_coe] using! Set.exists_of_ssubset

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ IsEmpty α ↔ s = ∅

Tactic:
by
  refine ⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩
  constructor
  intro x
  simp only [IsMaxChain, h', IsChain.empty, empty_subset, forall_const, true_and] at h
  exact singleton_ne_empty x (h IsChain.singleton).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s

Tactic:
rw [Icc_self, mem_singleton_iff] at hz

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m

Tactic:
refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩

Goal state after:
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

pp: case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
· rfl

Goal state after:
case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) = f (y / x)

Tactic:
rw [← inv_div, map_inv_eq_map]

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

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
replace hn : 0 < (n : k) := by norm_cast

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ ⌈a⌉ ≤ ⌊a⌋ + 1

Tactic:
rw [ceil_le, Int.cast_add, Int.cast_one]

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a ≤ ↑⌊a⌋ + 1
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1

Tactic:
exact n.cast_add_one_pos

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ fract (f a) = f (fract a)

Tactic:
by
  simp_rw [fract, map_sub, map_intCast, map_floor _ hf]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ • p₁ = v₂ • p₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂

Tactic:
by
  rw [eq_smul_iff_sdiv_eq, smul_sdiv_assoc, ← mul_right_inj v₁⁻¹, inv_mul_cancel_left, eq_comm]

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x : P
⊢ ∀ (x_1 : P), (Equiv.symm (pointReflection x)) x_1 = (pointReflection x) x_1

Tactic:
by simp [pointReflection]

Goal state after: