mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ (↑s).PairwiseDisjoint fun a ↦ (f a).disjUnion (g a) ⋯

Tactic:
intros i hi j hj hij

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
i : α
hi : i ∈ ↑s
j : α
hj : j ∈ ↑s
hij : i ≠ j
⊢ Function.onFun Disjoint (fun a ↦ (f a).disjUnion (g a) ⋯) i j
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
induction s using Multiset.induction <;> simp [Int.add_emod, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)

Tactic:
simp_rw [disjoint_disjiUnion_left, disjoint_disjiUnion_right]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ ∀ i ∈ s, ∀ i_1 ∈ s, Disjoint (f i) (g i_1)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (s.sigma t).card = (map (fun a ↦ (t a).card) s).sum

Tactic:
by
  simp [Multiset.sigma, (· ∘ ·)]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]
  cases n <;> rfl; apply zero_lt_succ

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

Goal state before:
pp: ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
classical
  let ⟨m⟩ := @Pi.instNonempty ι π _
  exact Infinite.of_injective _ (update_injective m i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
⊢ ∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (cons m a b₁ f₁ a_1 ha) (cons m a b₂ f₂ a_1 ha)

Tactic:
by
  intro a ha
  dsimp [cons]
  split_ifs with H
  · cases H
    exact hb
  · exact hf _ _

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

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((t a).val.bind fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup

Tactic:
congr

Goal state after:
case e_f
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)) = fun b ↦
    (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
x : X
⊢ ∀ (y : X), ∃ g, g • x = y

Tactic:
y

Goal state after:
G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
x y : X
⊢ ∃ g, g • x = y
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x : α
⊢ ∀ (y : α), ∃ g, g • x = y

Tactic:
y

Goal state after:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x y : α
⊢ ∃ g, g • x = y
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ (ConjClasses.mk b).carrier ↔ ConjClasses.mk a = ConjClasses.mk b

Tactic:
carrier,

Goal state after:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ Quotient.lift conjugatesOf ⋯ (ConjClasses.mk b) ↔ ConjClasses.mk a = ConjClasses.mk b
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s carrier✝¹ : Set M
mul_mem'✝¹ : ∀ {a b : M}, a ∈ carrier✝¹ → b ∈ carrier✝¹ → a * b ∈ carrier✝¹
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ }.carrier = { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ } = { carrier := carrier✝, mul_mem' := mul_mem'✝ }

Tactic:
congr

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x : M
⊢ ∀ (b : M), x = b

Tactic:
y

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ x = y
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S

Tactic:
rw [pow_zero]

Goal state after:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ i, s i
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ ⋃ i, s i → f x = f x₂ → x = x₂

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ i, s i
y : α
⊢ y ∈ ⋃ i, s i → f x = f y → x = y
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i✝ : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
i : ι
⊢ a i = b i

Tactic:
exact pow_left_injective hn <| congr_fun hab i

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
⊢ ∀ (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
y

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter <;> gcongr <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Set α
t : Set β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
by simp [pow_succ, prod_pow _ _ n]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
hp : Set G
mul_mem'✝¹ : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem'✝¹ : 1 ∈ { carrier := hp, mul_mem' := mul_mem'✝¹ }.carrier
inv_mem'✝¹ :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹ }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹ }.carrier
hq : Set G
mul_mem'✝ : ∀ {a b : G}, a ∈ hq → b ∈ hq → a * b ∈ hq
one_mem'✝ : 1 ∈ { carrier := hq, mul_mem' := mul_mem'✝ }.carrier
inv_mem'✝ :
  ∀ {x : G},
    x ∈ { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      x⁻¹ ∈ { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
    (fun s ↦ s.carrier) { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ }
⊢ { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
    { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
p : ι → Subgroup G
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
simp_rw [closure_iUnion, closure_eq]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x : ↥H₁ × ↥H₂
⊢ ∀ ⦃a₂ : ↥H₁ × ↥H₂⦄, (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) a₂ → x = a₂

Tactic:
y

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
⊢ (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) y → x = y
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.succ.bodd = !n.bodd

Tactic:
simp only [bodd]
  cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y

Tactic:
by rw [← encodek, e, encodek]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ a • B ↔ a⁻¹ • A ⊆ B

Tactic:
refine (image_subset_iff.trans ?_).symm

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun x ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₂
⊢ ∀ (y : G₂), g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)

Tactic:
y

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
⊢ b * a ∈ H

Tactic:
by
  have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
  rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this

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

Goal state before:
pp: α : Type ?u.3
s t : Set α
h✝ : s ⊆ t
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : (fun x ↦ ⟨↑x, ⋯⟩) ⟨x, hx⟩ = (fun x ↦ ⟨↑x, ⋯⟩) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
congr

Goal state after:
α : Type ?u.3
s t : Set α
h✝ : s ⊆ t
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : (fun x ↦ ⟨↑x, ⋯⟩) ⟨x, hx⟩ = (fun x ↦ ⟨↑x, ⋯⟩) ⟨y, hy⟩
⊢ x = y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
⊢ ∀ (y : N) (z : α), ((x * x') • y) • z = (x * x') • y • z

Tactic:
y

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
y : N
⊢ ∀ (z : α), ((x * x') • y) • z = (x * x') • y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
⊢ ∀ (n : N) (a : α), (x * x') • n • a = n • (x * x') • a

Tactic:
y

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
⊢ ∀ (a : α), (x * x') • y • a = y • (x * x') • a
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
toFun✝¹ : α → β
map_top'✝¹ : toFun✝¹ ⊤ = ⊤
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝¹, map_top' := map_top'✝¹ }.toFun = { toFun := toFun✝, map_top' := map_top'✝ }.toFun
⊢ { toFun := toFun✝¹, map_top' := map_top'✝¹ } = { toFun := toFun✝, map_top' := map_top'✝ }

Tactic:
congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_top'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊤ = ⊤
map_bot'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
BoundedOrderHom.comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun = { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } = { toFun := toFun✝, map_sup' := map_sup'✝ }

Tactic:
congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun (a ⊓ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun a ⊓ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }

Tactic:
congr

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

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b

Tactic:
· rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Max α
inst✝⁶ : Bot α
inst✝⁵ : Max β
inst✝⁴ : Bot β
inst✝³ : Max γ
inst✝² : Bot γ
inst✝¹ : Max δ
inst✝ : Bot δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_bot'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_sup' := map_sup'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_bot' := map_bot'✝ }

Tactic:
congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun (a ⊓ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun a ⊓ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun b
map_top'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun ⊤ = ⊤
map_bot'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹,
        map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min' ⋯ = a

Tactic:
by simp [min']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).max ≠ ↑x

Tactic:
by
  by_cases! s0 : (s.erase x).Nonempty
  · refine ne_of_eq_of_ne (coe_max' s0).symm ?_
    exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
  · rw [s0, max_empty]
    exact WithBot.bot_ne_coe

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

Goal state before:
pp: α : Type u
l : List α
x✝ : α
y✝ : Array (List α)
⊢ (Array.foldl (fun r l ↦ r.push (x✝ :: l)) y✝.toList.toArray y✝.toList.toArray).toList =
    (Array.foldl (fun r l ↦ r.push (x✝ :: l)) y✝ y✝).toList

Tactic:
congr

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
⊢ ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
y

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → x < y → ∃ z ∈ t, x < z ∧ z < y
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
⊢ ∀ ⦃b : α⦄, b ∈ ↑s → x < b → f x < f b

Tactic:
y

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
⊢ y ∈ ↑s → x < y → f x < f y
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ (s.sup fun x ↦ ⊥) = ⊥

Tactic:
· exact sup_const hs _

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
⊢ ∀ ⦃y : α⦄, ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y

Tactic:
y

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
⊢ ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = (image f s).sup id

Tactic:
sup_image,

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = s.sup (id ∘ f)