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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c

Tactic:
by
  rw [inv_mul_le_iff₀ hc, mul_comm]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x

Tactic:
and_iff_left_of_imp h.trans_lt',

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b < x ∨ x < a ↔ x < a ∨ b < x
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ↪r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ (b a : α), i.toEmbedding b ≤ i.toEmbedding a ↔ b ≤ a

Tactic:
exact @i.2

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ↪r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ (b a : α), i.toEmbedding a ≤ i.toEmbedding b ↔ a ≤ b

Tactic:
exact @i.2

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ (b a : α), i.toEquiv b ≤ i.toEquiv a ↔ b ≤ a

Tactic:
exact @i.2

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ≃r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ (b a : α), i.toEquiv a ≤ i.toEquiv b ↔ a ≤ b

Tactic:
exact @i.2

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

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n * (m * r % k) % k = r % k

Tactic:
mul_mod,

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n % k * (m * r % k % k) % k = r % k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n * m * r % k = r % k

Tactic:
mul_mod,

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n * m % k * (r % k) % k = r % k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ c ^ (n * m) = (c ^ m) ^ n

Tactic:
← pow_mul'

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ c ^ (n * m) = c ^ (n * m)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
exact ⟨0, by simp_all⟩

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
· rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_add_self

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ Surjective ⇑(map' f) ↔ Surjective ⇑f

Tactic:
by
  simp only [Surjective, «forall»]
  refine ⟨fun h b ↦ ?_, fun h ↦ ⟨⟨0, by simp⟩, fun b ↦ ?_⟩⟩
  · obtain ⟨a, hab⟩ := h.2 b
    induction a using WithZero.recZeroCoe <;>
    simp at hab
    grind
  · obtain ⟨a, ha⟩ := h b
    use a
    simp [ha]

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 : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
refine le_antisymm ?_ le_add_tsub
  obtain ⟨c, rfl⟩ := exists_add_of_le h
  grw [add_tsub_le_left]

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 : α
h : a ≤ b
⊢ b - a + a = b

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) = b
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 c : α
h : c ≤ a
h2 : a - c < a - c
⊢ False

Tactic:
exact h2.false

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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c
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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
rw [add_comm]
  exact ha.le_tsub_iff_left h

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 : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
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 : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = b ↔ a ≤ b

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c

Tactic:
· exact zero_le

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
⊢ 0 * b ≤ 0 * c

pp: case coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ * b ≤ ↑a✝ * c

Tactic:
· exact zero_le

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ * b ≤ ↑a✝ * c
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ * 0 ≤ ↑a✝ * c

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * c

Tactic:
· exact zero_le

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * c
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: m k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n

Tactic:
induction k generalizing m with
  | zero =>
    rw [eq_comm, Iff.comm]
    simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
    rintro rfl
    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩
  | succ k ihk =>
    by_cases hk : P (k + 1)
    · rw [findGreatest_eq hk]
      constructor
      · rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩
      · rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]
    · rw [findGreatest_of_not hk, ihk]
      grind

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : FloorSemiring R
z : ℤ
a : ℕ
⊢ ⌈↑z⌉₊ ≤ a ↔ z.toNat ≤ a

Tactic:
by
    simp only [ceil_le, Int.toNat_le]
    norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
by_cases ha : IsUnit a

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

case neg
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
by_cases ha : IsUnit a

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

case neg
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulLeft₀ c hc).map_sup a b

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ k * a ^ k ↔ a ≠ 0

Tactic:
mul_self_pos,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ a ^ k ≠ 0 ↔ a ≠ 0
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b

Tactic:
rw [← dvd_neg, neg_sub]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

Tactic:
by
  simpa only [one_div] using (inv_sub_inv' ha hb).symm

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
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ StrictMono fun a ↦ a ^ n

Tactic:
by
  have hn₀ : n ≠ 0 := by rintro rfl; simp [Odd] at hn
  intro a b hab
  obtain ha | ha := le_total 0 a
  · exact pow_lt_pow_left₀ hab ha hn₀
  obtain hb | hb := lt_or_ge 0 b
  · exact (hn.pow_nonpos ha).trans_lt (pow_pos hb _)
  obtain ⟨c, hac⟩ := exists_add_of_le ha
  obtain ⟨d, hbd⟩ := exists_add_of_le hb
  have hd := nonneg_of_le_add_right (hb.trans_eq hbd)
  refine lt_of_add_lt_add_right (a := c ^ n + d ^ n) ?_
  dsimp
  calc
    a ^ n + (c ^ n + d ^ n) = d ^ n := by
      rw [← add_assoc, hn.pow_add_pow_eq_zero hac.symm, zero_add]
    _ < c ^ n := pow_lt_pow_left₀ ?_ hd hn₀
    _ = b ^ n + (c ^ n + d ^ n) := by rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]
  refine lt_of_add_lt_add_right (a := a + b) ?_
  rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n * max |a| |b|

Tactic:
mul_comm |a|

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |geomSum a b n| * |a| ≤ (↑n + 1) * max |a| |b| ^ n * max |a| |b|
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)

Tactic:
by
  simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case inl
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : a ≤ b
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

Tactic:
exact (h.trans h₂.le).symmGen

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
⊢ ¬BddAbove (Set.range f)

Tactic:
by
  rintro ⟨a, ha⟩
  obtain ⟨b, hb⟩ := exists_gt a
  exact ((hf.le_apply.trans_lt (hf hb)).trans_le <| ha (Set.mem_range_self _)).false

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
by rw [eq, of_decide_eq_true h]; simp

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
by rw [eq, of_decide_eq_true h]; simp

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod

Tactic:
induction l with

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
l : List ι
⊢ (map (fun x ↦ 1) l).prod = 1

Tactic:
induction l with

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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : l ≠ []
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c < a ↔ a * c < b

Tactic:
div_lt_iff_of_neg hc

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a * c < b ↔ a * c < b
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ drop (l.length - 1) l = [l.getLast h]

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
x✝ : List α
b : γ
u : List γ
⊢ Forall₂ R x✝ (map f (b :: u)) ↔ Forall₂ (fun a c ↦ R a (f c)) x✝ (b :: u)

Tactic:
simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]

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

Goal state before:
pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)

pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)

pp: case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
· exact SublistForall₂.nil

Goal state after:
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)

case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
⊢ Perm ∘r Perm = Perm

Tactic:
funext a c

Goal state after:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
b : β
⊢ foldr f b l₁ = foldr f b l₂

Tactic:
induction p using Perm.recOnSwap' generalizing b with

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

Goal state before:
pp: case mpr
α : Type u
⊢ Subsingleton α → Injective length

Tactic:
intro hα l1 l2 hl
    induction l1 generalizing l2 <;> cases l2
    · rfl
    · cases hl
    · cases hl
    · next ih _ _ =>
      congr
      · subsingleton
      · apply ih; simpa using hl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l

Tactic:
induction l with

Goal state after:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun x ↦ f x ++ g x) (a :: l)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.getLast? = l.getLast?

Tactic:
← List.head?_reverse,

Goal state after:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.reverse.head? = l.getLast?
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.reverse.head? = l.getLast?

Tactic:
← List.head?_reverse,

Goal state after:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.reverse.head? = l.reverse.head?
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
⊢ l[0]?.getD 1 * l.tail.prod = l.prod

Tactic:
by
  cases l <;> simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y l.prod

Tactic:
induction l with

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

Goal state before:
pp: α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a :: l = x :: (a :: l).tail

Tactic:
by
    simp only [head?, Option.mem_def, Option.some_inj] at h
    exact h ▸ rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1

Tactic:
induction l with

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
a : M
inst✝ : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
induction l with

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ idxOf a l₁ ≤ idxOf a l₂

Tactic:
by
  obtain ⟨l₃, rfl⟩ := hl
  grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <:+ l₂
a : α
⊢ idxOf a l₂ ≤ l₂.length - l₁.length + idxOf a l₁

Tactic:
by
  obtain ⟨l₃, rfl⟩ := hl
  grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <:+ l₂
a : α
⊢ idxOf a l₂ + l₁.length ≤ idxOf a l₁ + l₂.length

Tactic:
by
  obtain ⟨l₃, rfl⟩ := hl
  grind

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
h : [].length - 1 < [].length
⊢ False

Tactic:
exact Nat.lt_irrefl 0 h

Goal state after: