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₀
hb : 0 < b
hc : 0 < c
⊢ a / b ≤ c ↔ a / c ≤ b

Tactic:
by
  rw [div_le_iff₀ hb, div_le_iff₀' hc]

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

Goal state before:
pp: case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
· exact RelHomClass.acc (Quotient.mkRelHom H) a

Goal state after:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y

Tactic:
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]

Goal state after:
case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
exact (lt_irrefl (1 : G) <| ha.trans_lt <| hab.trans_lt hb).elim

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

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rw [mabs_of_one_le <| one_le_div'.mpr h]

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ b / d ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (-(1 + ↑k * 2)) = -a ^ (-(1 + ↑k * 2))

Tactic:
_root_.zpow_neg

Goal state after:
case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ ((-a) ^ (1 + ↑k * 2))⁻¹ = -(a ^ (1 + ↑k * 2))⁻¹
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ gcdB 0 s = 1

Tactic:
rw [gcdB, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: α : 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
ha : ¬a = 0
| a ^ 1

Tactic:
rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]

Goal state after:
α : 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
ha : ¬a = 0
| a ^ (↑m * m.gcdA n + ↑n * m.gcdB n)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : 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
ha : ¬a = 0
| b ^ 1

Tactic:
rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]

Goal state after:
α : 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
ha : ¬a = 0
| b ^ (↑m * m.gcdA n + ↑n * m.gcdB n)
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = 0 ↔ a = 0

Tactic:
by
  conv_lhs => rw [← mul_zero b]
  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective ((fun x ↦ a * x) ∘ fun x ↦ b * x)

Tactic:
rwa [comp_mul_left a b]

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 < b + c

Tactic:
exact hb.tsub_lt_iff_left hba

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : α
hm : Even m
hn : Even n
⊢ Even (m - n)

Tactic:
obtain ⟨a, rfl⟩ := hm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n : α
hn : Even n
a : α
⊢ Even (a + a - n)
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ 0 ≤ ↑(n - m) ↔ m ≤ n

Tactic:
cast_nonneg_iff,

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ 0 ≤ n - m ↔ m ≤ n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case zero
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬0 = 0 → P 0) ∧ ∀ ⦃n : ℕ⦄, 0 < n → n = 0 → ¬P n

Tactic:
exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩

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

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : toAdd (unzero h) = b
⊢ a = ↑(ofAdd b)

Tactic:
subst k; exact (coe_unzero h).symm

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
⊢ 0 < ⌈a⌉₊ ↔ 0 < a

Tactic:
lt_ceil,

Goal state after:
α : Type u_2
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
⊢ ↑0 < a ↔ 0 < a
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 < ⌈a⌉ ↔ 0 < a

Tactic:
lt_ceil,

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ ↑0 < a ↔ 0 < a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
exact cast_le.1 ((floor_le ha).trans <| le_ceil _)

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ 0 < ⌈b⌉₊

Tactic:
lt_ceil,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ↑0 < b
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * c = b ↔ a = b * ⅟c

Tactic:
by
  rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (f r)
⊢ f ⅟r = ⅟(f r)

Tactic:
obtain rfl : ifr = Invertible.map f r := Subsingleton.elim _ _; rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp_all

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
by_cases h : a = 0
  · simp [h, map_zero f]
  · apply eq_inv_of_mul_eq_one_left
    rw [← map_mul, inv_mul_cancel₀ h, map_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ (a + a) / 2 = a

Tactic:
by
  rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤ
hu : IsUnit u
⊢ u = 1 ∨ u = -1

Tactic:
by
  simpa only [natAbs_of_isUnit hu] using! natAbs_eq u

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u v : ℤ
h : u * v = 1
h' : v * u = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h <;>
      obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'

Goal state after:
case inl.inl
h h' : 1 * 1 = 1
⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1

case inl.inr
h : 1 * -1 = 1
h' : -1 * 1 = 1
⊢ 1 = 1 ∧ -1 = 1 ∨ 1 = -1 ∧ -1 = -1

case inr.inl
h : -1 * 1 = 1
h' : 1 * -1 = 1
⊢ -1 = 1 ∧ 1 = 1 ∨ -1 = -1 ∧ 1 = -1

case inr.inr
h h' : -1 * -1 = 1
⊢ -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = f ↑q.num / f ↑q.den

Tactic:
natCast,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = ↑q.num / f ↑q.den
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
⊢ ↑q = ↑q.num / f ↑q.den

Tactic:
natCast,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)

Tactic:
exact fun q hq =>
      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s ∪ t \ s = t

Tactic:
by simp [union_sdiff_self, union_eq_self_of_subset_left h]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
⊢ Ioo a b ∪ {a, b} = Icc a b

Tactic:
rw [← this, Icc_sdiff_both]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t

Tactic:
rw [directedOn_union_iff] at h
  tauto

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

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
· exact .inl ⟨h, hs⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedGT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f = g

Tactic:
change f.dual.dual = g.dual.dual

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedGT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f.dual.dual = g.dual.dual
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedGT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f = g

Tactic:
change f.dual.dual = g.dual.dual

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedGT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f.dual.dual = g.dual.dual
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
⊢ a = c ∧ b = d → Icc a b = Icc c d

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ a ≤ x

Tactic:
convert h (x / b) ((one_lt_div hb).mpr hbx)

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ x = b * (x / b)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
⊢ (a, b) ∈ (a :: l₁).zip (b :: l₂)

Tactic:
simp [zip]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
⊢ (map f l).eraseIdx n = map f (l.eraseIdx n)

Tactic:
simpa only [pmap_eq_map] using eraseIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) n

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b = 2 * a * b * (ε * ε⁻¹)

Tactic:
mul_inv_cancel₀ hε.ne',

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b = 2 * a * b * 1
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge (length l₁) n with
  | inl hn₁ =>
    rw [insertIdx_of_length_lt hn₁]
    cases Nat.lt_or_ge (length l₂) n with
    | inl hn₂ => rw [insertIdx_of_length_lt hn₂]
    | inr hn₂ =>
      apply iff_of_false
      · intro h
        rw [h.length_eq] at hn₁
        grind
      · grind [Perm.length_eq]
  | inr hn₁ =>
    exact perm_insertIdx_iff_of_le hn₁ (Nat.le_trans hn₁ hle) _

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

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

Tactic:
induction l

Goal state after:
case nil
α : Type u
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ []).flatten.head? = [].head?

case cons
α : Type u
n : ℕ
h : n.succ ≠ 0
head✝ : α
tail✝ : List α
tail_ih✝ : (replicate n.succ tail✝).flatten.head? = tail✝.head?
⊢ (replicate n.succ (head✝ :: tail✝)).flatten.head? = (head✝ :: tail✝).head?
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h₁ : l₁ ≠ []
h₂ : l₂ ≠ []
h₃ : l₁ = l₂
⊢ l₁.getLast h₁ = l₂.getLast h₂

Tactic:
by subst l₁; rfl

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 : α
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · exact hl.idxOf_eq_of_mem h ▸ idxOf_lt_length_of_mem h
  · have := hl.idxOf_le a
    grind [List.idxOf_lt_length_iff]

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

Goal state before:
pp: M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
l : List M
⊢ (filter (fun x ↦ x != 1) l).prod = l.prod

Tactic:
induction l

Goal state after:
case nil
M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
⊢ (filter (fun x ↦ x != 1) []).prod = [].prod

case cons
M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
head✝ : M
tail✝ : List M
tail_ih✝ : (filter (fun x ↦ x != 1) tail✝).prod = tail✝.prod
⊢ (filter (fun x ↦ x != 1) (head✝ :: tail✝)).prod = (head✝ :: tail✝).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| xs.prod * ys.prod

Tactic:
prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| (zipWith (fun x1 x2 ↦ x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun x ↦ x⁻¹) (map (fun k ↦ f (k + 1) / f k) (range n))).prod = (f n / f 0)⁻¹

Tactic:
map_map,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) (range n)).prod = (f n / f 0)⁻¹
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
induction l

Goal state after:
case nil
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []

case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α) (b : β), f (foldl op₁ a tail✝) (foldl op₂ b tail✝) = foldl op₃ (f a b) tail✝
⊢ ∀ (a : α) (b : β),
    f (foldl op₁ a (head✝ :: tail✝)) (foldl op₂ b (head✝ :: tail✝)) = foldl op₃ (f a b) (head✝ :: tail✝)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
induction l

Goal state after:
case nil
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])

case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α), foldr op₃ (f a b) tail✝ = f (foldr op₁ a tail✝) (foldr op₂ b tail✝)
⊢ ∀ (a : α), foldr op₃ (f a b) (head✝ :: tail✝) = f (foldr op₁ a (head✝ :: tail✝)) (foldr op₂ b (head✝ :: tail✝))