awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update (β := β) f a' v = update (β := β) f a' v'
this : update (β := β) f a' v a' = update (β := β) f a' v' a'
rwa : ∀ (this : v = update (β := β) f a' v' a'), v = v'
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : v = v'), v = v'
⊢ v = v'

Tactic:
rwa [update_self, update_self] at this

Premises used: Function.update_self
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
rw : (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update (β := β) f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
⊢ (∀ (x : α), p x (update (β := β) f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
rw [← and_forall_ne a, update_self]

Premises used: and_forall_ne, Function.update_self
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update (β := β) f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
simp +contextual
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
rw : ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)
⊢ (∃ (x : α), p x (update (β := β) f a b x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)

Tactic:
rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]

Premises used: not_forall_not, Function.forall_update_iff, Not
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)

Tactic:
simp [-not_and, not_and_or]

Premises used: not_and_or, not_and
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
a : α
b : β a
f g : (a : α) → β a
⊢ update (β := β) f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x

Tactic:
funext_iff.trans <| forall_update_iff _ fun x y ↦ y = g x

Premises used: funext_iff, Function.forall_update_iff, Iff.trans, Eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
a : α
b : β a
f g : (a : α) → β a
⊢ g = update (β := β) f a b ↔ g a = b ∧ ∀ (x : α), x ≠ a → g x = f x

Tactic:
funext_iff.trans <| forall_update_iff _ fun x y ↦ g x = y

Premises used: funext_iff, Function.forall_update_iff, Iff.trans, Eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ update (β := β) f a b = f ↔ b = f a

Tactic:
simp [update_eq_iff]

Premises used: Function.update_eq_iff
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ f = update (β := β) f a b ↔ f a = b

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ f ≠ update (β := β) f a b ↔ f a ≠ b

Tactic:
eq_update_self_iff.not

Premises used: Iff.not, Function.eq_update_self_iff
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ update (β := β) f a b ≠ f ↔ b ≠ f a

Tactic:
update_eq_self_iff.not

Premises used: Iff.not, Function.update_eq_self_iff
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
a : α
f : (a : α) → β a
⊢ update (β := β) f a (f a) = f

Tactic:
update_eq_iff.2 ⟨rfl, fun _ _ ↦ rfl⟩

Premises used: Iff.mpr, Function.update_eq_iff, And.intro, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
α' : Sort u_1
g : (a : α) → β a
f : α' → α
i : α
a : β i
h : ∀ (x : α'), f x ≠ i
⊢ Eq (α := (j : α') → β (f j)) (fun (j : α') ↦ update (β := β) g i a (f j)) fun (j : α') ↦ g (f j)

Tactic:
funext fun _ ↦ update_of_ne (h _) _ _

Premises used: funext, Function.update_of_ne
-- Module: Mathlib.Logic.Function.Basic
Goal:
α' : Sort w
inst : DecidableEq α'
α : Sort u_1
β : Sort u_2
g : α' → β
f : α → α'
i : α'
a : β
h : ∀ (x : α), f x ≠ i
⊢ update (β := fun (a : α') ↦ β) g i a ∘ f = g ∘ f

Tactic:
update_comp_eq_of_forall_ne' g a h

Premises used: Function.update, dite, Function.update_comp_eq_of_forall_ne'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
α' : Sort w
inst : DecidableEq α
inst_1 : DecidableEq α'
g : (a : α) → β a
f : α' → α
hf : Injective f
i : α'
a : β (f i)
⊢ Eq (α := (j : α') → β (f j)) (fun (j : α') ↦ update (β := β) g (f i) a (f j))
    (update (β := fun (i : α') ↦ β (f i)) (fun (i : α') ↦ g (f i)) i a)

Tactic:
eq_update_iff.2 ⟨update_self .., fun _ hj ↦ update_of_ne (hf.ne hj) _ _⟩

Premises used: Iff.mpr, Function.Injective.ne, Function.eq_update_iff, And.intro, Function.update_self, Function.update_of_ne
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
α' : Sort w
inst : DecidableEq α
inst_1 : DecidableEq α'
g : (a : α) → β a
f : α' → α
hf : Injective f
i : α'
a : β (f i)
j : α'
⊢ Eq (α := β (f j)) (update (β := β) g (f i) a (f j))
    (update (β := fun (i : α') ↦ β (f i)) (fun (i : α') ↦ g (f i)) i a j)

Tactic:
congr_fun (update_comp_eq_of_injective' g hf i a) j

Premises used: congr_fun, Function.update_comp_eq_of_injective'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
α' : Sort w
inst : DecidableEq α
inst_1 : DecidableEq α'
β : Sort u_1
g : α' → β
f : α → α'
hf : Injective f
i : α
a : β
⊢ update (β := fun (a : α') ↦ β) g (f i) a ∘ f = update (β := fun (a : α) ↦ β) (g ∘ f) i a

Tactic:
update_comp_eq_of_injective' g hf i a

Premises used: Function.update, dite, Function.update_comp_eq_of_injective'
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
κ : Sort u_2
α : κ → Sort u_3
inst : DecidableEq ι
inst_1 : DecidableEq κ
ctor : ι → κ
h_1 : Injective ctor
recursor : ((i : ι) → α (ctor i)) → (i : κ) → α i
h : ∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i
h2 : ∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i ≠ k) → recursor f₁ k = recursor f₂ k
f : (i : ι) → α (ctor i)
i : ι
x : α (ctor i)
⊢ recursor (update (β := fun (i : ι) ↦ α (ctor i)) f i x) = update (β := α) (recursor f) (ctor i) x

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
β : Option α → Sort u_2
inst : DecidableEq α
f : β none
g : (a : α) → β (some a)
a : α
x : β (some a)
⊢ (fun (t : Option α) ↦
      Option.rec (motive := fun (x : Option α) ↦ β x) f (update (β := fun (val : α) ↦ β (some val)) g a x) t) =
    update (β := β) (fun (t : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ β x) f g t) (some a) x

Tactic:
Function.rec_update (@Option.some.inj _) (Option.rec f) (fun _ _ => rfl) (fun
    | _, _, some _, h => (h _ rfl).elim
    | _, _, none, _ => rfl) _ _ _

Premises used: False.elim, _private.0.Option.rec_update.match_1, Option.some.inj, Option.rec, Function.rec_update, Eq, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update (β := α) g i v j) = update (β := β) (fun (k : ι) ↦ f k (g k)) i (f i v) j

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update (β := α) g i v j) (update (β := β) h i w j) =
    update (β := γ) (fun (k : ι) ↦ f k (g k) (h k)) i (f i v w) j

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
P : ⦃a : α⦄ → β a → Prop
f : (a : α) → β a
a' : α
v : β a'
a : α
⊢ P (update (β := β) f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
inst : DecidableEq α
α' : Sort u_1
β : Sort u_2
f : α' → β
g : α → α'
i : α
v : α'
⊢ f ∘ update (β := fun (a : α) ↦ α') g i v = update (β := fun (a : α) ↦ β) (f ∘ g) i (f v)

Tactic:
funext <| apply_update _ _ _ _

Premises used: Function.apply_update, funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_2
inst : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (β := β) (update (β := β) f a v) b w = update (β := β) (update (β := β) f b w) a v

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_2
inst : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (β := β) (update (β := β) f a v) a w = update (β := β) f a w

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
h :
  ∀ (j : ι),
    Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j
⊢ Pi.map (α := α) (β := β) f (update (β := α) g i a) = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a)

Tactic:
ext j
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
h :
  ∀ (a : α j),
    Pi.map (α := α) (β := β) f (update (β := α) g j a) j = update (β := β) (Pi.map (α := α) (β := β) f g) j (f j a) j
h₁ :
  ∀ (hij : j ≠ i),
    Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j
⊢ Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j

Tactic:
obtain rfl | hij := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
j : ι
a : α j
⊢ Pi.map (α := α) (β := β) f (update (β := α) g j a) j = update (β := β) (Pi.map (α := α) (β := β) f g) j (f j a) j

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
inst : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
hij : j ≠ i
⊢ Pi.map (α := α) (β := β) f (update (β := α) g i a) j = update (β := β) (Pi.map (α := α) (β := β) f g) i (f i a) j

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
have : ∀ (this : Inhabited ((i : ι) → α i)), x = y
⊢ x = y

Tactic:
have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
refine_2 : ∀ (h : update (β := α) default i x = update (β := α) default i y), x = y
refine_1 :
  Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
⊢ x = y

Tactic:
replace h := @h (Function.update default i x) (Function.update default i y) ?_
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update (β := α) default i x = update (β := α) default i y
⊢ x = y

Tactic:
simpa using congrFun h i

Premises used: congrFun
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
refine_1 :
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
    Pi.map (α := α) (β := β) f (update (β := α) default i y)
refine_1₁ :
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i x) =
    update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y)
refine_1₂ refine_1₃ :
  update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y) =
    update (β := β) (Pi.map (α := α) (β := β) f default) i (f i y)
⊢ Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)

Tactic:
rw [Pi.map_update, Pi.map_update, hxy]

Premises used: Pi.map_update
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst : ∀ (i : ι), Nonempty.{u_2} (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map (α := α) (β := β) f)
i : ι
x y : α i
hxy : f i x = f i y
have have₁ have₂ : ∀ (this : Inhabited ((i : ι) → α i)), x = y
refine_2 : ∀ (this : Inhabited ((i : ι) → α i)) (h : update (β := α) default i x = update (β := α) default i y), x = y
refine_1 refine_1₁ :
  ∀ (this : Inhabited ((i : ι) → α i)),
    Pi.map (α := α) (β := β) f (update (β := α) default i x) = Pi.map (α := α) (β := β) f (update (β := α) default i y)
⊢ x = y

Tactic:
classical
    have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
    replace h := @h (Function.update default i x) (Function.update default i y) ?_
    · simpa using congrFun h i
    rw [Pi.map_update, Pi.map_update, hxy]

Premises used: Pi.map_update
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst : Decidable (∃ (a : α), f a = b)
unfold :
  Eq.{u_3} (α := γ) (if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b)
    (if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b)
⊢ extend f g e' b = if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b

Tactic:
unfold extend

Premises used: Function.extend
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst : Decidable (∃ (a : α), f a = b)
⊢ Eq.{u_3} (α := γ) (if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b)
    (if h : ∃ (a : α), f a = b then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else e' b)

Tactic:
congr
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
g : α → γ
⊢ FactorsThrough g f

Tactic:
fun _ _ h => congr_arg g (hf h)

Premises used: Function.FactorsThrough, congr_arg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
simp : g (Classical.choose (p := fun (x : α) ↦ f x = f a) ⋯) = g a
⊢ extend f g e' (f a) = g a

Tactic:
simp only [extend_def, dif_pos, exists_apply_eq_apply]

Premises used: Function.extend_def, dif_pos, exists_apply_eq_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ g (Classical.choose (p := fun (x : α) ↦ f x = f a) ⋯) = g a

Tactic:
hf (Classical.choose_spec (exists_apply_eq_apply f a))

Premises used: Classical.choose_spec, exists_apply_eq_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ g (Classical.choose (p := fun (x : α) ↦ f x = f a) ⋯) = g a

Tactic:
exact hf (Classical.choose_spec (exists_apply_eq_apply f a))

Premises used: Classical.choose_spec, exists_apply_eq_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
simp : g (Classical.choose (p := fun (x : α) ↦ f x = f a) ⋯) = g a
⊢ extend f g e' (f a) = g a

Tactic:
classical
  simp only [extend_def, dif_pos, exists_apply_eq_apply]
  exact hf (Classical.choose_spec (exists_apply_eq_apply f a))

Premises used: Function.extend_def, dif_pos, Classical.choose_spec, exists_apply_eq_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
g : α → γ
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a

Tactic:
(hf.factorsThrough g).extend_apply e' a

Premises used: Function.FactorsThrough.extend_apply, Function.Injective.factorsThrough
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ (a : α), f a = b
⊢ extend f g e' b = e' b

Tactic:
simp [Function.extend_def, hb]

Premises used: Function.extend_def
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ (a : α), f a = b
⊢ extend f g e' b = e' b

Tactic:
classical
  simp [Function.extend_def, hb]

Premises used: Function.extend_def
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
γ : Sort u_3
g e' : α → γ
⊢ extend id g e' = g

Tactic:
funext <| injective_id.extend_apply g _

Premises used: Function.Injective.extend_apply, Function.injective_id, funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
h : ∀ (a : α₃), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
⊢ extend (f₂₃ ∘ f₁₂) g e' = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e'

Tactic:
ext a
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
pos : ∀ (h₃ : ∃ (b : α₂), f₂₃ b = a), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
neg : ∀ (h₃ : ¬∃ (b : α₂), f₂₃ b = a), extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
by_cases h₃ : ∃ b, f₂₃ b = a
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ∃ (b : α₂), f₂₃ b = a
pos : ∀ (b : α₂), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' (f₂₃ b)
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
obtain ⟨b, rfl⟩ := h₃

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
pos : extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' (f₂₃ b)

Tactic:
rw [Injective.extend_apply h₂₃]

Premises used: Function.Injective.extend_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
pos : ∀ (h₂ : ∃ (c : α₁), f₁₂ c = b), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
neg : ∀ (h₂ : ¬∃ (c : α₁), f₁₂ c = b), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
by_cases h₂ : ∃ c, f₁₂ c = b
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ∃ (c : α₁), f₁₂ c = b
pos : ∀ (c : α₁), extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
obtain ⟨c, rfl⟩ := h₂

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
pos : extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)

Tactic:
rw [h₁₂.extend_apply]

Premises used: Function.Injective.extend_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c

Tactic:
(h₂₃.comp h₁₂).extend_apply _ _ _

Premises used: Function.Injective.extend_apply, Function.Injective.comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c

Tactic:
exact (h₂₃.comp h₁₂).extend_apply _ _ _

Premises used: Function.Injective.extend_apply, Function.Injective.comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ (c : α₁), f₁₂ c = b
neg : ¬∃ (a : α₁), (f₂₃ ∘ f₁₂) a = f₂₃ b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]

Premises used: Function.extend_apply', Function.comp_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ (c : α₁), f₁₂ c = b
⊢ ¬∃ (a : α₁), (f₂₃ ∘ f₁₂) a = f₂₃ b

Tactic:
fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))

Premises used: Exists.casesOn, Not
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ (c : α₁), f₁₂ c = b
⊢ ¬∃ (a : α₁), (f₂₃ ∘ f₁₂) a = f₂₃ b

Tactic:
exact fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))

Premises used: Exists.casesOn
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ (b : α₂), f₂₃ b = a
neg : ¬∃ (a_1 : α₁), (f₂₃ ∘ f₁₂) a_1 = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
rw [extend_apply' _ _ _ h₃, extend_apply']

Premises used: Function.extend_apply'
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ (b : α₂), f₂₃ b = a
⊢ ¬∃ (a_1 : α₁), (f₂₃ ∘ f₁₂) a_1 = a

Tactic:
fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))

Premises used: Exists.casesOn, Not
-- Module: Mathlib.Logic.Function.Basic
Goal:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ (b : α₂), f₂₃ b = a
⊢ ¬∃ (a_1 : α₁), (f₂₃ ∘ f₁₂) a_1 = a

Tactic:
exact fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))

Premises used: Exists.casesOn
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x

Tactic:
simp only [comp_apply, hf.extend_apply]

Premises used: Function.FactorsThrough.extend_apply, Function.comp_apply